52.16 Algebraization of… to 52.24 Application to the…

Section52.16 Algebraization of coherent formal modules, I#

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

Tag 0EHC, a situation

Tag 0EHC in the Stacks Project.

Stacks.Algebraization.AlgebraizationSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationSituation.lean, line 59. The attribute's comment: “the ring and ideals”.

Stacks Project, Tag 0EHC (standing data). A Noetherian ring with nested ideals I ⊆ 𝔞.

public structure AlgebraizationSituation

Stacks.Algebraization.AlgebraizationSituation.X, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationSituation.lean, line 79. The attribute's comment: “the scheme X”.

Stacks Project, Tag 0EHC (X). The affine scheme X = Spec(A).

public abbrev X (S : AlgebraizationSituation) : Scheme

Stacks.Algebraization.AlgebraizationSituation.Y, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationSituation.lean, line 83. The attribute's comment: “the closed subscheme Y”.

Stacks Project, Tag 0EHC (Y). The closed subscheme Y = V(I) = Spec(A/I).

public abbrev Y (S : AlgebraizationSituation) : Scheme

Stacks.Algebraization.AlgebraizationSituation.Z, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationSituation.lean, line 87. The attribute's comment: “the closed subscheme Z”.

Stacks Project, Tag 0EHC (Z). The closed subscheme Z = V(𝔞) = Spec(A/𝔞).

public abbrev Z (S : AlgebraizationSituation) : Scheme

Stacks.Algebraization.AlgebraizationSituation.U, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationSituation.lean, line 112. The attribute's comment: “the open complement U”.

Stacks Project, Tag 0EHC (U). The open subset U = X \ Z, namely the complement of V(𝔞) in Spec(A).

public def U (S : AlgebraizationSituation) : S.X.Opens

Tag 0DXT, a lemma

Tag 0DXT in the Stacks Project.

Stacks.Algebraization.restrictedTildeSystem_isCoherentAdicSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/FiniteModuleModel.lean, line 1012. The attribute's comment: “forward implication”.

A finite module model gives a coherent adic system on the punctured spectrum.

public theorem restrictedTildeSystem_isCoherentAdicSystem
    (M : ℕᵒᵖ ⥤ ModuleCat.{u} S.A) (hM : IsFiniteModuleModel S M) :
    Stacks.Coherent.IsCoherentAdicSystem (Stacks.Algebraization.idealOnOpen S)
      (restrictedTildeSystem S M)

Stacks.Algebraization.exists_finiteModuleModel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/FiniteModuleModel.lean, line 1029. The attribute's comment: “converse”.

Every coherent adic system on U has a finite module model, compatible with the whole inverse-system structure.

public theorem exists_finiteModuleModel
    (F : Stacks.Coherent.CoherentAdicSystems (Stacks.Algebraization.idealOnOpen S)) :
    ∃ M : ℕᵒᵖ ⥤ ModuleCat.{u} S.A,
      ∃ hM : IsFiniteModuleModel S M,
        Nonempty (coherentAdicSystemOfFiniteModuleModel S M hM ≅ F)

Tag 0EIK, an equation

Tag 0EIK in the Stacks Project.

Stacks.Algebraization.completionFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionFunctor/Basic.lean, line 475. The attribute's comment: “the same completion functor on an open subscheme, at the restricted ideal”.

Completion of a coherent sheaf along a quasi-coherent ideal, as a coherent adic inverse system.

public noncomputable def completionFunctor (X : Scheme.{u})
    [AlgebraicGeometry.IsLocallyNoetherian X] (I : X.IdealSheafData) :
    AlgebraicGeometry.SheafOfModules.CoherentModules X.ringCatSheaf ⥤
      Stacks.Coherent.CoherentAdicSystems I

Tag 0EIL, a lemma

Tag 0EIL in the Stacks Project.

Stacks.Algebraization.isRestrictionOfCompletion_of_extendsToX, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionCriteria/AffineExistence.lean, line 250. The attribute's comment: “extendable implies restriction of a completion”.

Stacks 0EIL, condition (6) implies condition (5) when A is I-adically complete.

public theorem isRestrictionOfCompletion_of_extendsToX (S : AlgebraizationSituation.{u})
    [IsAdicComplete S.I S.A]
    (F : Stacks.Coherent.CoherentAdicSystems (S.Yι.ker.comap S.U.ι))
    (h : ExtendsToX S F) : IsRestrictionOfCompletion S F

Stacks.Algebraization.isCompletion_iff_nearClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionCriteria/Algebraization.lean, line 225. The attribute's comment: “completion iff near the closed subscheme”.

Stacks 0EIL, conditions (2) and (3) are equivalent. A coherent adic system on U is the completion of a coherent module on U exactly when it is the completion of a coherent module on some open neighbourhood of U ∩ Y in U.

One direction takes the neighbourhood to be U itself. For the other, a coherent module on the neighbourhood V extends to U, and the two systems — the completion of the extension and the given one — are then isomorphic over V; every term of either is annihilated by a power of the ideal and so is supported inside V, and restriction to V is fully faithful on modules supported there, so the isomorphism over V comes from an isomorphism over U.

public theorem isCompletion_iff_nearClosed (S : AlgebraizationSituation.{u})
    (F : Stacks.Coherent.CoherentAdicSystems (S.Yι.ker.comap S.U.ι)) :
    (completionFunctor S.U.toScheme (S.Yι.ker.comap S.U.ι)).essImage F ↔
      IsCompletionNearClosed S F

Stacks.Algebraization.isCompletion_iff_ofRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionCriteria/Algebraization.lean, line 262. The attribute's comment: “completion iff completion of a restriction”.

Stacks 0EIL, conditions (2) and (4) are equivalent. A coherent adic system on U is the completion of a coherent module on U exactly when it is the completion of one that extends to a coherent module on X.

X is affine and Noetherian, so every coherent module on the open U is the restriction of a coherent module on X; the converse direction forgets the extension.

public theorem isCompletion_iff_ofRestriction (S : AlgebraizationSituation.{u})
    (F : Stacks.Coherent.CoherentAdicSystems (S.Yι.ker.comap S.U.ι)) :
    (completionFunctor S.U.toScheme (S.Yι.ker.comap S.U.ι)).essImage F ↔
      IsCompletionOfRestriction S F

Stacks.Algebraization.isCompletionOfRestriction_iff_isRestrictionOfCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionCriteria/Algebraization.lean, line 276. The attribute's comment: “the two restriction conditions agree”.

Stacks 0EIL, conditions (4) and (5) are equivalent. Being the completion of a module restricted from X is the same as being the restriction of a completion on X, because completion commutes with restriction to an open.

public theorem isCompletionOfRestriction_iff_isRestrictionOfCompletion
    (S : AlgebraizationSituation.{u})
    (F : Stacks.Coherent.CoherentAdicSystems (S.Yι.ker.comap S.U.ι)) :
    IsCompletionOfRestriction S F ↔ IsRestrictionOfCompletion S F

Stacks.Algebraization.extendsToX_of_isRestrictionOfCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionCriteria/Algebraization.lean, line 291. The attribute's comment: “restriction of a completion extends to X”.

Stacks 0EIL, condition (5) implies condition (6). A system that is the restriction of a completion on X extends to X: the completion itself is the extension.

public theorem extendsToX_of_isRestrictionOfCompletion (S : AlgebraizationSituation.{u})
    (F : Stacks.Coherent.CoherentAdicSystems (S.Yι.ker.comap S.U.ι))
    (h : IsRestrictionOfCompletion S F) : ExtendsToX S F

Tag 0EHE, an example

Tag 0EHE in the Stacks Project.

Stacks.Algebraization.NonAlgebraizableExample.idealPowerQuotientIsoPushforwardPullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableAlgebraizing.lean, line 316. The attribute's comment: “L/I^n L is the direct image along Spec(A/t^n A) ∩ U → U of the pullback of L”.

Stacks Project, Tag 0EHE (the level comparison). For a quasi-coherent 𝒪_U-module 𝓛 the term 𝓛 / Iⁿ𝓛 is the direct image along levelStructureMap k n of the pullback of 𝓛: the closed immersion Spec(A/tⁿA) ∩ U ⟶ U has kernel ideal sheaf (I𝒪_U)ⁿ (ker_levelStructureMap), which is exactly the hypothesis of [Stacks, Tag 0EL1].

public def idealPowerQuotientIsoPushforwardPullback (n : ℕ)
    (M : (situation k).U.toScheme.Modules) [M.IsQuasicoherent] :
    idealPowerQuotient (idealOnOpen (situation k)) n M ≅
      (Scheme.Modules.pushforward (levelStructureMap k n)).obj
        ((Scheme.Modules.pullback (levelStructureMap k n)).obj M)

Stacks.Algebraization.NonAlgebraizableExample.idealPowerQuotientIsoPushforwardPullbackOnOpen, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableAlgebraizing.lean, line 329. The attribute's comment: “L/I^n L is the direct image of the pullback of L restricted to a smaller open”.

Stacks Project, Tag 0EHE (the level comparison through an intermediate open). The same identification, with the pullback taken in two steps through an open V ⊆ U that levelStructureMap k n factors through: 𝓛 / Iⁿ𝓛 is the direct image of the pullback of 𝓛|_V.

public def idealPowerQuotientIsoPushforwardPullbackOnOpen (n : ℕ)
    (M : (situation k).U.toScheme.Modules) [M.IsQuasicoherent]
    (V : (situation k).U.toScheme.Opens) (f : (levelOpen k n).toScheme ⟶ V.toScheme)
    (hf : f ≫ V.ι = levelStructureMap k n) :
    idealPowerQuotient (idealOnOpen (situation k)) n M ≅
      (Scheme.Modules.pushforward (levelStructureMap k n)).obj
        ((Scheme.Modules.pullback f).obj ((Scheme.Modules.pullback V.ι).obj M))

Stacks.Algebraization.NonAlgebraizableExample.not_isCompletionOfCoherent_levelCoherentAdicSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableAlgebraizing.lean, line 376. The attribute's comment: “the family (L_n) is not the completion of a coherent O_U-module”.

Stacks Project, Tag 0EHE (the family is not algebraizable). The object (𝓛ₙ) of Coh(U, I𝒪_U) is not the completion of any coherent 𝒪_U-module, for every choice of the coefficients aₘ and the exponents φ(m).

This is the source's first proof. An algebraizing coherent module 𝓛 has invertible stalks along U ∩ Y, so it is invertible on an open V with U ∩ Y ⊆ V ⊆ U (exists_isInvertibleModule_restrict_of_isInvertibleAdic_completionIso); there it is trivial, A = k[x,y][[t]] being a unique factorization domain (isTrivial_of_isInvertible_ambientOpen); the level-two term of its completion is the direct image along the closed immersion of the punctured spectrum of A/t²A of the pullback of 𝓛|_V (idealPowerQuotientIsoPushforwardPullbackOnOpen), hence of the structure sheaf, and direct image along a closed immersion is fully faithful, so 𝓛₂ ≅ 𝒪; and not_isTrivial_levelModule_two forbids that.

public theorem not_isCompletionOfCoherent_levelCoherentAdicSystem (a : ℕ → PlaneRing k)
    (φ : ℕ → ℕ) :
    ¬ IsCompletionOfCoherent (idealOnOpen (situation k)) (levelCoherentAdicSystem k a φ)

Stacks.Algebraization.NonAlgebraizableExample.isLocalization_away_levelToChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableChartLocalization.lean, line 74. The attribute's comment: “A_r/t^n A_r is the localization of A/t^n A away from the image of r”.

Stacks Project, Tag 0EHE (the chart rings). The chart ring A_r/t^nA_r is the localization of the level ring A/t^nA away from the image of r, so it is the ring of sections of O on the basic open D(r) of Spec(A/t^nA).

public theorem isLocalization_away_levelToChart (r : AmbientRing k) (n : ℕ) :
    letI : Algebra (levelRing k n) (chartRing k r n) := (levelToChart k r n).toAlgebra
    IsLocalization.Away (Ideal.Quotient.mk ((idealT k) ^ n) r) (chartRing k r n)

Stacks.Algebraization.NonAlgebraizableExample.map_chartOpenEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableChartSections.lean, line 75. The attribute's comment: “restriction from D(r) to D(q) is A_r/t^n A_r -> A_q/t^n A_q”.

Restriction of chart functions along a divisibility. On the sections of 𝒪 over the basic opens of Spec(A/tⁿA), restriction from D(r̄) to the smaller D(q̄) is the map A_r/tⁿA_r → A_q/tⁿA_q.

public theorem map_chartOpenEquiv (r q : AmbientRing k) (hdvd : r ∣ q) (n : ℕ)
    (hle : chartOpen k q n ≤ chartOpen k r n) (v : chartRing k r n) :
    ((levelScheme k n).presheaf.map (homOfLE hle).op).hom (chartOpenEquiv k r n v) =
      chartOpenEquiv k q n (chartRestrict k r q hdvd n v)

Stacks.Algebraization.NonAlgebraizableExample.levelChartRingEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableChartSections.lean, line 110. The attribute's comment: “A_r/t^n A_r is the ring of sections of O on the chart D(r)”.

Stacks Project, Tag 0EHE (a chart ring is the ring of sections on the chart). The chart ring A_r/tⁿA_r is the ring of sections of 𝒪 on the chart D(r̄) of the punctured spectrum of A/tⁿA; compare levelOverlapRingEquiv for the overlap of the two charts.

public def levelChartRingEquiv (r : AmbientRing k) (n : ℕ)
    (hle : chartOpen k r n ≤ levelOpen k n) :
    chartRing k r n ≃+* Γ((levelOpen k n).toScheme, levelChart k r n)

Stacks.Algebraization.NonAlgebraizableExample.map_levelChartRingEquiv_overlap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableChartSections.lean, line 131. The attribute's comment: “restriction from a chart to the overlap is A_r/t^n A_r -> A_xy/t^n A_xy”.

Stacks Project, Tag 0EHE (restriction from a chart to the overlap). Restriction of sections of 𝒪 from a chart of the punctured spectrum of A/tⁿA to the overlap of the two charts is the map chartRestrict of chart rings. This is the dictionary between the sheaf-level and the ring-level description of the glued module: a global section of 𝓛ₙ is a pair of chart functions matched on the overlap, and this is what matching means.

public theorem map_levelChartRingEquiv_overlap (r : AmbientRing k) (n : ℕ)
    (hdvd : r ∣ xVar k * yVar k) (hle : chartOpen k r n ≤ levelOpen k n)
    (hq : chartOpen k (xVar k * yVar k) n ≤ chartOpen k r n)
    (h : levelOverlap k n ≤ levelChart k r n) (v : chartRing k r n) :
    ((levelOpen k n).toScheme.presheaf.map (homOfLE h).op).hom
        (levelChartRingEquiv k r n hle v) =
      levelOverlapRingEquiv k n (chartRestrict k r (xVar k * yVar k) hdvd n v)

Stacks.Algebraization.NonAlgebraizableExample.situation, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableExample.lean, line 128. The attribute's comment: “the situation A = k[x,y][[t]], I = (t), 𝔞 = (x,y,t)”.

Stacks Project, Tag 0EHE (the situation). The algebraization situation with A = k[x,y][[t]], I = (t) and 𝔞 = (x,y,t).

public def situation : AlgebraizationSituation.{u}

Stacks.Algebraization.NonAlgebraizableExample.coe_U_inter_zeroLocus_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableExample.lean, line 151. The attribute's comment: “the open covering of U ∩ Y by D(x) and D(y)”.

Stacks Project, Tag 0EHE (the two-chart covering). The punctured closed fibre U ∩ Y of the situation is covered by the two basic opens D(x) and D(y). Each of D(x) ∩ Y and D(y) ∩ Y is affine, being a basic open of an affine scheme; see AlgebraicGeometry.IsAffineOpen.basicOpen.

public theorem coe_U_inter_zeroLocus_eq :
    (situation k).U.carrier ∩
        PrimeSpectrum.zeroLocus ((idealT k : Ideal (AmbientRing k)) : Set (AmbientRing k)) =
      ((PrimeSpectrum.basicOpen (xVar k)).carrier ∪
          (PrimeSpectrum.basicOpen (yVar k)).carrier) ∩
        PrimeSpectrum.zeroLocus ((idealT k : Ideal (AmbientRing k)) : Set (AmbientRing k))

Stacks.Algebraization.NonAlgebraizableExample.compl_zeroLocus_map_idealXYT, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableExample.lean, line 211. The attribute's comment: “the two charts D(x), D(y) cover the punctured spectrum of A/t^n”.

Stacks Project, Tag 0EHE (the two charts cover the punctured spectrum of A/t^n). The element t is nilpotent in A/t^nA, hence lies in every prime, so the vanishing locus of 𝔞 = (x,y,t) in Spec(A/t^nA) is the vanishing locus of (x,y). Its complement — the part of Spec(A/t^nA) lying over U — is therefore the union of the two basic opens D(x) and D(y), and no third chart is needed to cover it.

public theorem compl_zeroLocus_map_idealXYT (n : ℕ) :
    (PrimeSpectrum.zeroLocus
        (((idealXYT k).map (Ideal.Quotient.mk ((idealT k) ^ n)) : Ideal (levelRing k n)) :
          Set (levelRing k n)))ᶜ =
      (PrimeSpectrum.basicOpen (Ideal.Quotient.mk ((idealT k) ^ n) (xVar k))).carrier ∪
        (PrimeSpectrum.basicOpen (Ideal.Quotient.mk ((idealT k) ^ n) (yVar k))).carrier

Stacks.Algebraization.NonAlgebraizableExample.isUnit_transitionElement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableExample.lean, line 273. The attribute's comment: “the transition element is a unit of A_xy/t^n A_xy”.

Stacks Project, Tag 0EHE (invertibility of the transition element). The transition element is a unit of A_{xy}/t^nA_{xy}: it is 1 plus a nilpotent element, every term beyond the leading 1 being divisible by t.

public theorem isUnit_transitionElement (a : ℕ → PlaneRing k) (φ : ℕ → ℕ) (n : ℕ) :
    IsUnit (transitionElement k a φ n)

Stacks.Algebraization.NonAlgebraizableExample.chartReduction_transitionElement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableExample.lean, line 303. The attribute's comment: “the transition elements are compatible with reduction mod t^n”.

Stacks Project, Tag 0EHE (the transition tower). The transition elements are compatible with reduction modulo t^n, so the glued modules form an inverse system.

public theorem chartReduction_transitionElement (a : ℕ → PlaneRing k) (φ : ℕ → ℕ) (n : ℕ) :
    chartReduction k (xVar k * yVar k) n (transitionElement k a φ (n + 1)) =
      transitionElement k a φ n

Stacks.Algebraization.NonAlgebraizableExample.exists_ne_zero_compatible_mem_gluedSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableExample.lean, line 556. The attribute's comment: “for a_m = 0 the functions x and x + t/y glue to a nonzero compatible system”.

Stacks Project, Tag 0EHE (nonzero limit of global sections for a_m = 0). When the higher coefficients a_m vanish, the function x on D(x) and the function x + t/y on D(y) glue at every order to a system of glued sections which is compatible with the reductions modulo t^n and is nonzero at every positive order. This is the source's reason that lim H⁰(U, L_n) is nonzero for this choice of coefficients.

public theorem exists_ne_zero_compatible_mem_gluedSections (a : ℕ → PlaneRing k) (φ : ℕ → ℕ)
    (ha : ∀ m : ℕ, 2 ≤ m → a m = 0) :
    ∃ s : (n : ℕ) → chartRing k (xVar k) n × chartRing k (yVar k) n,
      (∀ n : ℕ, s n ∈ gluedSections k n (transitionElement k a φ n)) ∧
      (∀ n : ℕ, (chartReduction k (xVar k) n (s (n + 1)).1,
        chartReduction k (yVar k) n (s (n + 1)).2) = s n) ∧
      ∀ n : ℕ, 0 < n → s n ≠ 0

Stacks.Algebraization.NonAlgebraizableExample.not_isUnit_of_mem_gluedSections_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableExample.lean, line 919. The attribute's comment: “modulo t^2 no pair of invertible chart functions is matched”.

Stacks Project, Tag 0EHE (nontriviality of the glued module at order two). The glued module at order two is not free: no pair consisting of an invertible function on D(x) and an invertible function on D(y), both taken modulo t², is matched by the transition element. The obstruction is that 1/(xy) is not a sum of a function on D(x) and a function on D(y).

public theorem not_isUnit_of_mem_gluedSections_two (a : ℕ → PlaneRing k) (φ : ℕ → ℕ)
    (s : chartRing k (xVar k) 2 × chartRing k (yVar k) 2)
    (hs : s ∈ gluedSections k 2 (transitionElement k a φ 2)) :
    ¬ (IsUnit s.1 ∧ IsUnit s.2)

Stacks.Algebraization.NonAlgebraizableExample.hasSeparatedExponents_of_eq_two_pow_or_sq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableExample.lean, line 1014. The attribute's comment: “phi(m) = 2^m and phi(m) = m^2 separate degrees”.

Stacks Project, Tag 0EHE (both prescribed growth rates separate degrees). The exponents φ(m) = 2ᵐ and the exponents φ(m) = m² both satisfy HasSeparatedExponents: the index n = p + 3 works for either, since p < 2^{p+2} and p < 2p + 5.

public theorem hasSeparatedExponents_of_eq_two_pow_or_sq {φ : ℕ → ℕ}
    (hφ : (∀ m : ℕ, 2 ≤ m → φ m = 2 ^ m) ∨ (∀ m : ℕ, 2 ≤ m → φ m = m ^ 2)) :
    HasSeparatedExponents φ

Stacks.Algebraization.NonAlgebraizableExample.sectionsLimit_eq_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableExample.lean, line 1295. The attribute's comment: “lim H^0(U, L_n) = 0 for a_m = 1 and φ(m) = 2^m or m^2”.

Stacks Project, Tag 0EHE (vanishing limit of global sections). When every higher coefficient a_m is 1 and the exponents are φ(m) = 2^m or φ(m) = m², the limit lim H⁰(U, L_n) of the global sections of the glued modules is zero.

public theorem sectionsLimit_eq_bot (a : ℕ → PlaneRing k) (φ : ℕ → ℕ)
    (ha : ∀ m : ℕ, 2 ≤ m → a m = 1)
    (hφ : (∀ m : ℕ, 2 ≤ m → φ m = 2 ^ m) ∨ (∀ m : ℕ, 2 ≤ m → φ m = m ^ 2)) :
    sectionsLimit k a φ = ⊥

Stacks.Algebraization.NonAlgebraizableExample.hasNonAlgebraizableInvertibleObject, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableInvertibleObject.lean, line 181. The attribute's comment: “Coh(U, I O_U) contains an invertible object which is not the completion of a coherent O_U-module”.

Stacks Project, Tag 0EHE. The category Coh(U, I𝒪_U) of the situation A = k[x,y][[t]], I = (t), 𝔞 = (x,y,t) contains an invertible object which is not the completion of any coherent 𝒪_U-module.

The witness is the family (𝓛ₙ) of the example, Stacks.Algebraization.NonAlgebraizableExample.levelCoherentAdicSystem, with the source's own choice aₘ = 1, φ(m) = 2ᵐ of parameters — though neither clause depends on that choice. Invertibility is Stacks.Algebraization.NonAlgebraizableExample.isInvertibleAdic_levelCoherentAdicSystem and non-algebraizability is not_isCompletionOfCoherent_levelCoherentAdicSystem.

public theorem hasNonAlgebraizableInvertibleObject : HasNonAlgebraizableInvertibleObject k

Stacks.Algebraization.NonAlgebraizableExample.chartOpenEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelChart.lean, line 94. The attribute's comment: “A_r/t^n A_r is the ring of sections of O on D(r) in Spec(A/t^n A)”.

The chart ring A_r/tⁿA_r is the ring of sections of 𝒪 on the basic open D(r̄) of Spec(A/tⁿA), as A/tⁿA-algebras.

public def chartOpenEquiv (r : AmbientRing k) (n : ℕ) :
    chartRing k r n ≃ₐ[levelRing k n] Γ(levelScheme k n, chartOpen k r n)

Stacks.Algebraization.NonAlgebraizableExample.coe_levelOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelChart.lean, line 107. The attribute's comment: “D(x) union D(y) is the part of Spec(A/t^n A) lying over U”.

The union of the two charts is the part of Spec(A/tⁿA) lying over U, namely the complement of the vanishing locus of the image of 𝔞 = (x,y,t).

public theorem coe_levelOpen (n : ℕ) :
    (levelOpen k n : Set (levelScheme k n)) =
      (PrimeSpectrum.zeroLocus
        (((idealXYT k).map (Ideal.Quotient.mk ((idealT k) ^ n)) : Ideal (levelRing k n)) :
          Set (levelRing k n)))ᶜ

Stacks.Algebraization.NonAlgebraizableExample.levelModule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelChart.lean, line 173. The attribute's comment: “the module L_n, glued from A_x/t^n A_x and A_y/t^n A_y along u”.

The module L_n: the sheaf of modules on the punctured spectrum of A/tⁿA glued from the two charts D(x̄) and D(ȳ) along the transition element u = 1 + t/(xy) + ∑_{m ≥ 2} aₘtᵐ/(xy)^{φ(m)}.

public def levelModule (a : ℕ → PlaneRing k) (φ : ℕ → ℕ) (n : ℕ) :
    (levelOpen k n).toScheme.Modules

Stacks.Algebraization.NonAlgebraizableExample.isInvertibleModule_levelModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelChart.lean, line 181. The attribute's comment: “L_n is an invertible module on the punctured spectrum of A/t^n A”.

The module L_n is an invertible module on the punctured spectrum of A/tⁿA.

public theorem isInvertibleModule_levelModule (a : ℕ → PlaneRing k) (φ : ℕ → ℕ) (n : ℕ) :
    Stacks.Ample.IsInvertibleModule (levelOpen k n).toScheme (levelModule k a φ n)

Stacks.Algebraization.NonAlgebraizableExample.ker_chartReduction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelChart.lean, line 187. The attribute's comment: “ker(A_r/t^(n+1) A_r -> A_r/t^n A_r) = t^n A_r/t^(n+1) A_r”.

The kernel of the reduction A_r/t^{n+1}A_r → A_r/tⁿA_r is tⁿ·A_r/t^{n+1}A_r.

public theorem ker_chartReduction (r : AmbientRing k) (n : ℕ) :
    LinearMap.ker (chartReduction k r n).toLinearMap =
      Ideal.span {algebraMap (AmbientRing k) (Localization.Away r) (tVar k)} ^ n •
        (⊤ : Submodule (Localization.Away r) (chartRing k r (n + 1)))

Stacks.Algebraization.NonAlgebraizableExample.preimage_U_levelToAmbient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelChart.lean, line 224. The attribute's comment: “the preimage of U in Spec(A/t^n A) is its punctured spectrum”.

The punctured spectrum of A/tⁿA is the preimage of the punctured spectrum U of A under the structure map Spec(A/tⁿA) ⟶ Spec(A).

public theorem preimage_U_levelToAmbient (n : ℕ) :
    levelToAmbient k n ⁻¹ᵁ (situation k).U = levelOpen k n

Stacks.Algebraization.NonAlgebraizableExample.levelModuleOnOpen, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelChart.lean, line 247. The attribute's comment: “L_n pushed forward to U along Spec(A/t^n A) ∩ U → U”.

The module L_n as a module on the punctured spectrum U of A: its direct image along the structure map levelStructureMap.

public def levelModuleOnOpen (a : ℕ → PlaneRing k) (φ : ℕ → ℕ) (n : ℕ) :
    (situation k).U.toScheme.Modules

Stacks.Algebraization.NonAlgebraizableExample.surjective_app_levelTransition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelEpi.lean, line 121. The attribute's comment: “L_(n+1) -> L_n is surjective on sections over an affine open of a chart”.

The transition map 𝓛ₙ₊₁ ⟶ (𝓛ₙ) is surjective on the sections over every affine open contained in one of the two charts.

public theorem surjective_app_levelTransition (a : ℕ → PlaneRing k) (φ : ℕ → ℕ) (n : ℕ)
    (i : ULift.{u} Bool) {V : (levelOpen k (n + 1)).toScheme.Opens}
    (hV : V ≤ Stacks.SheafOfModules.twoChartFamily
      (levelChart k (xVar k) (n + 1)) (levelChart k (yVar k) (n + 1)) i)
    (hVa : IsAffineOpen V) :
    Function.Surjective ((levelTransition k a φ n).val.app (op V))

Stacks.Algebraization.NonAlgebraizableExample.epi_levelTransition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelEpi.lean, line 146. The attribute's comment: “the transition map L_(n+1) -> L_n is an epimorphism”.

The transition map 𝓛ₙ₊₁ ⟶ (𝓛ₙ) of the system is an epimorphism of modules on the punctured spectrum of A/t^{n+1}A.

public theorem epi_levelTransition (a : ℕ → PlaneRing k) (φ : ℕ → ℕ) (n : ℕ) :
    Epi (levelTransition k a φ n)

Stacks.Algebraization.NonAlgebraizableExample.levelOpenMap_comp_levelStructureMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelEpi.lean, line 175. The attribute's comment: “the closed immersions of punctured spectra are compatible with the maps to U”.

The closed immersion of the punctured spectrum of A/tⁿA in that of A/t^{n+1}A, followed by the structure map of level n + 1 to U, is the structure map of level n.

public theorem levelOpenMap_comp_levelStructureMap (n : ℕ) :
    levelOpenMap k n ≫ levelStructureMap k (n + 1) = levelStructureMap k n

Stacks.Algebraization.NonAlgebraizableExample.levelTransitionOnOpen, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelEpi.lean, line 195. The attribute's comment: “the transition map L_(n+1) -> L_n of the system, as modules on U”.

The transition map 𝓛ₙ₊₁ ⟶ 𝓛ₙ of the system as a morphism of modules on the punctured spectrum U of A: the direct image along the structure map of level n + 1 of Stacks.Algebraization.NonAlgebraizableExample.levelTransition, read through Stacks.Algebraization.NonAlgebraizableExample.levelPushforwardIso.

public def levelTransitionOnOpen (a : ℕ → PlaneRing k) (φ : ℕ → ℕ) (n : ℕ) :
    levelModuleOnOpen k a φ (n + 1) ⟶ levelModuleOnOpen k a φ n

Stacks.Algebraization.NonAlgebraizableExample.preimage_levelStructureMap_ambientBasicOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelEpi.lean, line 248. The attribute's comment: “the preimage of D(h) in the punctured spectrum of A/t^n A is D(h)”.

The preimage of D(h) under the structure map Spec(A/tⁿA) ∩ U ⟶ U is the chart D(h̄) of the punctured spectrum of A/tⁿA.

public theorem preimage_levelStructureMap_ambientBasicOpen (h : AmbientRing k) (m : ℕ) :
    levelStructureMap k m ⁻¹ᵁ ambientBasicOpen k h = levelChart k h m

Stacks.Algebraization.NonAlgebraizableExample.exists_mem_basicOpen_of_mem_U, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelEpi.lean, line 280. The attribute's comment: “U is covered by D(x), D(y) and D(t)”.

The punctured spectrum U of A is covered by D(x), D(y) and D(t).

public theorem exists_mem_basicOpen_of_mem_U (p : (situation k).X)
    (hp : p ∈ (situation k).U) :
    p ∈ PrimeSpectrum.basicOpen (xVar k) ∨ p ∈ PrimeSpectrum.basicOpen (yVar k) ∨
      p ∈ PrimeSpectrum.basicOpen (tVar k)

Stacks.Algebraization.NonAlgebraizableExample.epi_levelTransitionOnOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelEpi.lean, line 334. The attribute's comment: “the transition map of the system on U is an epimorphism”.

The transition map 𝓛ₙ₊₁ ⟶ 𝓛ₙ of the system, read as a morphism of modules on the punctured spectrum U of A, is an epimorphism.

public theorem epi_levelTransitionOnOpen (a : ℕ → PlaneRing k) (φ : ℕ → ℕ) (n : ℕ) :
    Epi (levelTransitionOnOpen k a φ n)

Stacks.Algebraization.NonAlgebraizableExample.levelSystem, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelEpi.lean, line 370. The attribute's comment: “the system (L_n) as a diagram over the opposite of the naturals”.

The family (𝓛ₙ) as an inverse system of modules on the punctured spectrum U of A, assembled from the transition maps Stacks.Algebraization.NonAlgebraizableExample.levelTransitionOnOpen. Its n-th term is 𝓛ₙ₊₁, the module on the punctured spectrum of A/t^{n+1}A, matching the indexing of Stacks.Coherent.IsCoherentAdicSystem.

public def levelSystem (a : ℕ → PlaneRing k) (φ : ℕ → ℕ) :
    ℕᵒᵖ ⥤ (situation k).U.toScheme.Modules

Stacks.Algebraization.NonAlgebraizableExample.epi_levelSystem_map_succ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelEpi.lean, line 387. The attribute's comment: “the maps of the system (L_n) from level n+1 to level n are epimorphisms”.

The maps of the system from its (n + 1)-st term to its n-th one are epimorphisms.

public theorem epi_levelSystem_map_succ (a : ℕ → PlaneRing k) (φ : ℕ → ℕ) (n : ℕ) :
    Epi ((levelSystem k a φ).map (homOfLE (Nat.le_succ n)).op)

Stacks.Algebraization.NonAlgebraizableExample.appLE_levelStructureMap_chartOpenEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelKernel.lean, line 218. The attribute's comment: “the two routes from A into the sections of O over a chart agree”.

The two routes from A into a chart's sections agree. An element z of A, restricted to an open V of U and pulled back along the structure map Spec(A/tᵐA) ∩ U ⟶ U to an open P inside the chart D(r̄), is the image of z in the chart ring A_r/tᵐA_r read as a section of 𝒪 and restricted to P.

This is what joins the description of the ideal (I𝒪_U)(V) — the image of I under A → Γ(X, X) → Γ(U, V) — to the description of the chart rings, and so the identity the kernel computation of the transition maps rests on.

public theorem appLE_levelStructureMap_chartOpenEquiv (q : AmbientRing k) (m : ℕ)
    {V : (situation k).U.toScheme.Opens} {P : (levelOpen k m).toScheme.Opens}
    (e : P ≤ levelStructureMap k m ⁻¹ᵁ V)
    (e' : P ≤ (levelOpen k m).ι ⁻¹ᵁ chartOpen k q m) (z : AmbientRing k) :
    ((levelStructureMap k m).appLE V P e).hom
        (((situation k).U.ι.appLE ⊤ V le_top).hom
          ((Scheme.ΓSpecIso (CommRingCat.of (AmbientRing k))).inv.hom z)) =
      ((levelOpen k m).ι.appLE (chartOpen k q m) P e').hom
        (chartOpenEquiv k q m (levelToChart k q m (levelElt k z m)))

Stacks.Algebraization.NonAlgebraizableExample.app_levelOpenMap_appLE_ι_chartOpenEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelKernel.lean, line 308. The attribute's comment: “on an open over D(r) the closed immersion induces A_r/t^(m+1) -> A_r/t^m”.

The closed immersion of punctured spectra on a chart's sections. Over an open P of the punctured spectrum of A/t^{m+1}A whose image is the basic open D(r̄), the closed immersion of punctured spectra induces the reduction of chart rings A_r/t^{m+1}A_r → A_r/tᵐA_r.

This is the general-open analogue of Stacks.Algebraization.NonAlgebraizableExample.app_levelOverlapRingEquiv, which is the case of the overlap of the two charts.

public theorem app_levelOpenMap_appLE_ι_chartOpenEquiv (q : AmbientRing k) (m : ℕ)
    {P : (levelOpen k (m + 1)).toScheme.Opens}
    (e' : P ≤ (levelOpen k (m + 1)).ι ⁻¹ᵁ chartOpen k q (m + 1))
    (f' : levelOpenMap k m ⁻¹ᵁ P ≤ (levelOpen k m).ι ⁻¹ᵁ chartOpen k q m)
    (v : chartRing k q (m + 1)) :
    ((levelOpenMap k m).app P).hom
        (((levelOpen k (m + 1)).ι.appLE (chartOpen k q (m + 1)) P e').hom
          (chartOpenEquiv k q (m + 1) v)) =
      ((levelOpen k m).ι.appLE (chartOpen k q m) (levelOpenMap k m ⁻¹ᵁ P) f').hom
        (chartOpenEquiv k q m (chartReduction k q m v))

Stacks.Algebraization.NonAlgebraizableExample.exists_smul_of_app_levelTransitionOnOpen_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelKernel.lean, line 378. The attribute's comment: “a section of L_(m+1) killed by the transition map is t^m times a section”.

The hard half of the kernel computation. A section of 𝓛ₘ₊₁ over an open V of U whose preimage is a chart D(r̄) of the punctured spectrum of A/t^{m+1}A, killed by the transition map 𝓛ₘ₊₁ ⟶ 𝓛ₘ, is tᵐ times a section.

Both modules are trivialized over the chart by Stacks.Algebraization.NonAlgebraizableExample.chartLinearEquiv_levelTransition, the sections over the chart are the chart ring by Stacks.Algebraization.NonAlgebraizableExample.chartOpenEquiv, and there the statement is Stacks.Algebraization.NonAlgebraizableExample.ker_chartReduction. The factor tᵐ produced upstairs is the pullback of the restriction of t to V by Stacks.Algebraization.NonAlgebraizableExample.appLE_levelStructureMap_chartOpenEquiv.

public theorem exists_smul_of_app_levelTransitionOnOpen_eq_zero (a : ℕ → PlaneRing k)
    (φ : ℕ → ℕ) (m : ℕ) (q : AmbientRing k) (i : ULift.{u} Bool)
    (hq : PrimeSpectrum.basicOpen q ≤ (situation k).U)
    {V : (situation k).U.toScheme.Opens}
    (hPeq : levelStructureMap k (m + 1) ⁻¹ᵁ V = levelChart k q (m + 1))
    (hchart : levelChart k q (m + 1) ≤ Stacks.SheafOfModules.twoChartFamily
      (levelChart k (xVar k) (m + 1)) (levelChart k (yVar k) (m + 1)) i)
    (s : Γ(levelModuleOnOpen k a φ (m + 1), V))
    (hs : ((levelTransitionOnOpen k a φ m).val.app (op V)).hom s = 0) :
    ∃ y : Γ(levelModuleOnOpen k a φ (m + 1), V),
      s = ((situation k).U.ι.appLE ⊤ V le_top).hom
        ((Scheme.ΓSpecIso (CommRingCat.of (AmbientRing k))).inv.hom (tVar k)) ^ m • y

Stacks.Algebraization.NonAlgebraizableExample.ker_app_levelTransitionOnOpen_chart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelKernel.lean, line 488. The attribute's comment: “over a basic open inside a chart ker(L_(m+1) -> L_m) = I(V)^m L_(m+1)(V)”.

The kernel over a basic open inside a chart. Over an affine open V of U whose preimage upstairs is a chart of the punctured spectrum of A/t^{m+1}A, the kernel of the transition map 𝓛ₘ₊₁ ⟶ 𝓛ₘ is I(V)ᵐ 𝓛ₘ₊₁(V).

public theorem ker_app_levelTransitionOnOpen_chart (a : ℕ → PlaneRing k) (φ : ℕ → ℕ) (m : ℕ)
    (q : AmbientRing k) (i : ULift.{u} Bool)
    (hq : PrimeSpectrum.basicOpen q ≤ (situation k).U)
    (V : (situation k).U.toScheme.affineOpens)
    (hPeq : levelStructureMap k (m + 1) ⁻¹ᵁ (V : (situation k).U.toScheme.Opens) =
      levelChart k q (m + 1))
    (hchart : levelChart k q (m + 1) ≤ Stacks.SheafOfModules.twoChartFamily
      (levelChart k (xVar k) (m + 1)) (levelChart k (yVar k) (m + 1)) i) :
    LinearMap.ker ((levelTransitionOnOpen k a φ m).val.app
        (op (V : (situation k).U.toScheme.Opens))).hom =
      (idealOnOpen (situation k)).ideal V ^ m •
        (⊤ : Submodule Γ((situation k).U.toScheme, (V : (situation k).U.toScheme.Opens))
          Γ(levelModuleOnOpen k a φ (m + 1), (V : (situation k).U.toScheme.Opens)))

Stacks.Algebraization.NonAlgebraizableExample.ker_app_levelTransitionOnOpen_of_preimage_eq_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelKernel.lean, line 513. The attribute's comment: “over a basic open with empty preimage both sides of the kernel identity vanish”.

The kernel over a basic open meeting no chart. Over an affine open V of U whose preimage upstairs is empty — a D(ht), the image of t being nilpotent in A/t^{m+1}A — the kernel of the transition map 𝓛ₘ₊₁ ⟶ 𝓛ₘ is I(V)ᵐ 𝓛ₘ₊₁(V), both sides being submodules of a module with one element.

public theorem ker_app_levelTransitionOnOpen_of_preimage_eq_bot (a : ℕ → PlaneRing k)
    (φ : ℕ → ℕ) (m : ℕ) (V : (situation k).U.toScheme.affineOpens)
    (hbot : levelStructureMap k (m + 1) ⁻¹ᵁ (V : (situation k).U.toScheme.Opens) = ⊥) :
    LinearMap.ker ((levelTransitionOnOpen k a φ m).val.app
        (op (V : (situation k).U.toScheme.Opens))).hom =
      (idealOnOpen (situation k)).ideal V ^ m •
        (⊤ : Submodule Γ((situation k).U.toScheme, (V : (situation k).U.toScheme.Opens))
          Γ(levelModuleOnOpen k a φ (m + 1), (V : (situation k).U.toScheme.Opens)))

Stacks.Algebraization.NonAlgebraizableExample.ker_app_levelSystem_map_succ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelKernel.lean, line 536. The attribute's comment: “the kernel of the maps of the system over the basis of affine opens D(hg)”.

The kernel computation of the system. The kernel of the map of the system (𝓛ₙ) from its (n + 1)-st term to its n-th one, over a member D(hg) of the basis of affine opens, is I(V)^{n+1} times the sections of the (n + 1)-st term. This is the hypothesis hker of Stacks.Algebraization.isCoherentAdicSystem_of_basis_ker.

For g one of the two variables the preimage of D(hg) upstairs is a chart, where the chartwise computation applies; for g = t it is empty and both sides vanish.

public theorem ker_app_levelSystem_map_succ (a : ℕ → PlaneRing k) (φ : ℕ → ℕ) (n : ℕ)
    (V : (situation k).U.toScheme.affineOpens) (hV : V ∈ ambientBasicAffineOpens k) :
    LinearMap.ker (((levelSystem k a φ).map (homOfLE (Nat.le_succ n)).op).val.app
        (op (V : (situation k).U.toScheme.Opens))).hom =
      (idealOnOpen (situation k)).ideal V ^ (n + 1) •
        (⊤ : Submodule Γ((situation k).U.toScheme, (V : (situation k).U.toScheme.Opens))
          Γ((levelSystem k a φ).obj (op (n + 1)),
            (V : (situation k).U.toScheme.Opens)))

Stacks.Algebraization.NonAlgebraizableExample.isCoherentAdicSystem_levelSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelKernel.lean, line 567. The attribute's comment: “the system (L_n) is a coherent I O_U-adic system”.

The system lies in Coh(U, I𝒪_U). The family (𝓛ₙ), as a diagram over ℕᵒᵖ of modules on the punctured spectrum U of A, is a coherent I𝒪_U-adic system: its terms are coherent and annihilated by the successive powers of I𝒪_U, its transition maps are epimorphisms, and their kernels over the basis of affine opens D(hg) are the expected ideal multiples.

public theorem isCoherentAdicSystem_levelSystem (a : ℕ → PlaneRing k) (φ : ℕ → ℕ) :
    Stacks.Coherent.IsCoherentAdicSystem (idealOnOpen (situation k)) (levelSystem k a φ)

Stacks.Algebraization.NonAlgebraizableExample.levelCoherentAdicSystem, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelKernel.lean, line 578. The attribute's comment: “the family (L_n) as an object of Coh(U, I O_U)”.

The object of Coh(U, I𝒪_U). The family (𝓛ₙ) as an object of the category Coh(U, I𝒪_U) of coherent I𝒪_U-adic systems on the punctured spectrum U of A.

public def levelCoherentAdicSystem (a : ℕ → PlaneRing k) (φ : ℕ → ℕ) :
    Stacks.Coherent.CoherentAdicSystems (idealOnOpen (situation k))

Stacks.Algebraization.NonAlgebraizableExample.isInvertibleAdic_levelCoherentAdicSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelKernel.lean, line 591. The attribute's comment: “the object (L_n) of Coh(U, I O_U) is invertible”.

The object is invertible. The object (𝓛ₙ) of Coh(U, I𝒪_U) is invertible: its n-th term is the direct image of an invertible module on the closed subscheme V((I𝒪_U)^{n+1}) of U.

That subscheme is the punctured spectrum of A/t^{n+1}A by Stacks.Algebraization.NonAlgebraizableExample.exists_subschemeIso_levelOpen, compatibly with the two morphisms to U, and 𝓛ₙ₊₁ is invertible there by Stacks.Algebraization.NonAlgebraizableExample.isInvertibleModule_levelModule.

public theorem isInvertibleAdic_levelCoherentAdicSystem (a : ℕ → PlaneRing k) (φ : ℕ → ℕ) :
    Stacks.Coherent.IsInvertibleAdic (idealOnOpen (situation k))
      (levelCoherentAdicSystem k a φ)

Stacks.Algebraization.NonAlgebraizableExample.exists_isUnit_mem_gluedSections_of_iso_unit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelNontrivial.lean, line 89. The attribute's comment: “a trivialization of L_n is a matched pair of invertible chart functions”.

Stacks Project, Tag 0EHE (a trivialization of 𝓛ₙ is a pair of invertible chart functions). If the glued module 𝓛ₙ is isomorphic to the structure sheaf of the punctured spectrum of A/tⁿA, then the transition element matches a pair consisting of an invertible function on D(x̄) and an invertible function on D(ȳ).

public theorem exists_isUnit_mem_gluedSections_of_iso_unit (a : ℕ → PlaneRing k) (φ : ℕ → ℕ)
    (n : ℕ) (e : levelModule k a φ n ≅ Stacks.Ample.unitModule (levelOpen k n).toScheme) :
    ∃ s : chartRing k (xVar k) n × chartRing k (yVar k) n,
      s ∈ gluedSections k n (transitionElement k a φ n) ∧ IsUnit s.1 ∧ IsUnit s.2

Stacks.Algebraization.NonAlgebraizableExample.not_isTrivial_levelModule_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelNontrivial.lean, line 139. The attribute's comment: “L_2 is not isomorphic to the structure sheaf”.

Stacks Project, Tag 0EHE (𝓛₂ ≇ 𝒪). The glued module at order two is not trivial, for every choice of the coefficients aₘ and the exponents φ(m): a trivialization would match a pair of invertible chart functions by the transition element 1 + t/(xy), and not_isUnit_of_mem_gluedSections_two rules that out. This is the source's "𝓛₂ ≇ 𝒪_U/I²𝒪_U by construction".

public theorem not_isTrivial_levelModule_two (a : ℕ → PlaneRing k) (φ : ℕ → ℕ) :
    ¬ Nonempty (levelModule k a φ 2 ≅ Stacks.Ample.unitModule (levelOpen k 2).toScheme)

Stacks.Algebraization.NonAlgebraizableExample.not_nonempty_pullback_iso_levelModule_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelNontrivial.lean, line 151. The attribute's comment: “no invertible module on an open of Spec(A) pulls back to L_2”.

Stacks Project, Tag 0EHE (no line bundle on an open of Spec(A) pulls back to 𝓛₂). Let V be an open subscheme of Spec(A), A = k[x,y][[t]], let L be an invertible 𝒪_V-module, and let f be any morphism from the punctured spectrum of A/t²A to V. Then the pullback of L along f is not isomorphic to 𝓛₂: the pullback is trivial, because L itself is trivial — A being a UFD — and 𝓛₂ is not.

public theorem not_nonempty_pullback_iso_levelModule_two (a : ℕ → PlaneRing k) (φ : ℕ → ℕ)
    {V : (Spec (CommRingCat.of (AmbientRing k))).Opens}
    (f : (levelOpen k 2).toScheme ⟶ V.toScheme) (L : V.toScheme.Modules)
    (hL : Stacks.Ample.IsInvertibleModule V.toScheme L) :
    ¬ Nonempty ((Scheme.Modules.pullback f).obj L ≅ levelModule k a φ 2)

Stacks.Algebraization.NonAlgebraizableExample.not_nonempty_pullback_levelStructureMap_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelNontrivial.lean, line 167. The attribute's comment: “no invertible module on U restricts to L_2”.

Stacks Project, Tag 0EHE (the class of 𝓛₂ is not in the image of Pic(U)). The specialization of not_nonempty_pullback_iso_levelModule_two to the structure map of the punctured spectrum of A/t²A over the punctured spectrum U of A: no invertible 𝒪_U-module restricts to 𝓛₂.

public theorem not_nonempty_pullback_levelStructureMap_iso (a : ℕ → PlaneRing k) (φ : ℕ → ℕ)
    (L : (situation k).U.toScheme.Modules)
    (hL : Stacks.Ample.IsInvertibleModule (situation k).U.toScheme L) :
    ¬ Nonempty ((Scheme.Modules.pullback (levelStructureMap k 2)).obj L ≅ levelModule k a φ 2)

Stacks.Algebraization.NonAlgebraizableExample.ker_levelToAmbient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelSubscheme.lean, line 68. The attribute's comment: “Spec(A/t^n A) is the closed subscheme of Spec(A) cut out by I^n”.

The kernel ideal sheaf of the closed immersion Spec(A/tⁿA) ⟶ Spec(A) is the n-th power of the ideal sheaf attached to I = (t).

public theorem ker_levelToAmbient (n : ℕ) :
    (levelToAmbient k n).ker =
      Scheme.IdealSheafData.ofIdealTop ((idealT k).map
        (CommRingCat.Hom.hom (Scheme.ΓSpecIso (CommRingCat.of (AmbientRing k))).inv)) ^ n

Stacks.Algebraization.NonAlgebraizableExample.idealOnOpen_pow_eq_comap_ker, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelSubscheme.lean, line 79. The attribute's comment: “(I O_U)^n is the restriction to U of the ideal sheaf of Spec(A/t^n A)”.

The n-th power of the ideal sheaf I𝒪_U on the punctured spectrum of A is the restriction to U of the ideal sheaf cutting out Spec(A/tⁿA) in Spec(A).

public theorem idealOnOpen_pow_eq_comap_ker (n : ℕ) :
    idealOnOpen (situation k) ^ n = (levelToAmbient k n).ker.comap (situation k).U.ι

Stacks.Algebraization.NonAlgebraizableExample.exists_subschemeIso_levelOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelSubscheme.lean, line 90. The attribute's comment: “V((I O_U)^n) is the punctured spectrum of A/t^n A”.

The closed subscheme of the punctured spectrum U of A cut out by the n-th power of I𝒪_U is the punctured spectrum of A/tⁿA, compatibly with the two morphisms to U: the closed immersion of the subscheme and the structure map Stacks.Algebraization.NonAlgebraizableExample.levelStructureMap.

public theorem exists_subschemeIso_levelOpen (n : ℕ) :
    ∃ e : (idealOnOpen (situation k) ^ n).subscheme ≅ (levelOpen k n).toScheme,
      e.hom ≫ levelStructureMap k n = (idealOnOpen (situation k) ^ n).subschemeι

Stacks.Algebraization.NonAlgebraizableExample.ker_levelStructureMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelSystem.lean, line 135. The attribute's comment: “the kernel ideal sheaf of Spec(A/t^n A) ∩ U → U is (I O_U)^n”.

Stacks Project, Tag 0EHE (the level scheme over U is cut out by (I𝒪_U)ⁿ). The kernel ideal sheaf of the structure map Spec(A/tⁿA) ∩ U ⟶ U is the n-th power of I𝒪_U.

This is Stacks.Algebraization.NonAlgebraizableExample.exists_subschemeIso_levelOpen read as an equality of ideal sheaves: that identification is compatible with the two morphisms to U, and a kernel ideal sheaf does not change when the morphism is precomposed with an isomorphism.

public theorem ker_levelStructureMap (m : ℕ) :
    (levelStructureMap k m).ker = idealOnOpen (situation k) ^ m

Stacks.Algebraization.NonAlgebraizableExample.isCoherent_levelModuleOnOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelSystem.lean, line 148. The attribute's comment: “L_n, pushed forward to U, is a coherent module”.

Stacks Project, Tag 0EHE (𝓛ₙ is coherent on U). The module 𝓛ₙ, read on the punctured spectrum U of A, is coherent: it is invertible upstairs, hence coherent there by [Stacks, Tag 01XZ], and its direct image along the closed immersion Spec(A/tⁿA) ∩ U ⟶ U — a finite morphism — is coherent by [Stacks, Tag 01Y6].

public theorem isCoherent_levelModuleOnOpen (a : ℕ → PlaneRing k) (φ : ℕ → ℕ) (m : ℕ) :
    _root_.SheafOfModules.IsCoherent.{u} (levelModuleOnOpen k a φ m)

Stacks.Algebraization.NonAlgebraizableExample.isCoherent_levelSystem_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelSystem.lean, line 160. The attribute's comment: “the terms of the system (L_n) are coherent”.

Stacks Project, Tag 0EHE (the system has coherent terms). Every term of the system (𝓛ₙ) is a coherent module on U. This is the hypothesis hcoh of Stacks.Algebraization.isCoherentAdicSystem_of_basis_ker.

public theorem isCoherent_levelSystem_obj (a : ℕ → PlaneRing k) (φ : ℕ → ℕ) (n : ℕ) :
    _root_.SheafOfModules.IsCoherent.{u} ((levelSystem k a φ).obj (op n))

Stacks.Algebraization.NonAlgebraizableExample.idealPowerMultiple_levelModuleOnOpen_eq_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelSystem.lean, line 183. The attribute's comment: “L_n, pushed forward to U, is annihilated by (I O_U)^n”.

Stacks Project, Tag 0EHE (𝓛ₙ is annihilated by (I𝒪_U)ⁿ). The module 𝓛ₙ, read on U, is annihilated by the n-th power of I𝒪_U: that power is the kernel ideal sheaf of the closed immersion Spec(A/tⁿA) ∩ U ⟶ U by Stacks.Algebraization.NonAlgebraizableExample.ker_levelStructureMap, and the kernel of a closed immersion kills every direct image along it.

public theorem idealPowerMultiple_levelModuleOnOpen_eq_bot (a : ℕ → PlaneRing k) (φ : ℕ → ℕ)
    (m : ℕ) :
    idealPowerMultiple (idealOnOpen (situation k)) m (levelModuleOnOpen k a φ m) = ⊥

Stacks.Algebraization.NonAlgebraizableExample.idealPowerMultiple_levelSystem_obj_eq_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelSystem.lean, line 198. The attribute's comment: “the n-th term of the system (L_n) is annihilated by (I O_U)^(n+1)”.

Stacks Project, Tag 0EHE (the system is annihilated by the successive ideal powers). The n-th term of the system (𝓛ₙ) is annihilated by the (n + 1)-st power of I𝒪_U. This is the hypothesis hann of Stacks.Algebraization.isCoherentAdicSystem_of_basis_ker; the exponent matches because the n-th term of the system is 𝓛ₙ₊₁.

public theorem idealPowerMultiple_levelSystem_obj_eq_bot (a : ℕ → PlaneRing k) (φ : ℕ → ℕ)
    (n : ℕ) :
    idealPowerMultiple (idealOnOpen (situation k)) (n + 1) ((levelSystem k a φ).obj (op n)) = ⊥

Stacks.Algebraization.NonAlgebraizableExample.ambientBasicAffineOpens, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelSystem.lean, line 220. The attribute's comment: “the family of affine opens D(hg) of U, for g one of x, y, t”.

Stacks Project, Tag 0EHE (the family of affine opens the kernel computation runs on). The affine opens D(hg) of U, for h an element of A and g one of the three variables x, y, t. Over each of them the module 𝓛ₙ is trivialized — for g = x or g = y because D(hg) lies in a chart, for g = t because its preimage upstairs is empty — and they form a basis of the topology of U.

public def ambientBasicAffineOpens : Set (situation k).U.toScheme.affineOpens

Stacks.Algebraization.NonAlgebraizableExample.exists_mem_ambientBasicAffineOpens, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelSystem.lean, line 230. The attribute's comment: “the affine opens D(hg) are a basis of the topology of U”.

Stacks Project, Tag 0EHE (those affine opens are a basis). Every point of every open W of the punctured spectrum U of A has one of the affine opens D(hg) around it inside W: the basic opens D(h) of Spec(A) are a basis of U, and D(h) is cut down into U by whichever of D(x), D(y), D(t) contains the point. This is the hypothesis hS of Stacks.Algebraization.isCoherentAdicSystem_of_basis_ker.

public theorem exists_mem_ambientBasicAffineOpens
    (W : (situation k).U.toScheme.Opens) (x : (situation k).U.toScheme) (hx : x ∈ W) :
    ∃ V ∈ ambientBasicAffineOpens k, x ∈ (V : (situation k).U.toScheme.Opens) ∧
      (V : (situation k).U.toScheme.Opens) ≤ W

Stacks.Algebraization.NonAlgebraizableExample.preimage_levelChart, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelTransition.lean, line 117. The attribute's comment: “the preimage of the chart D(r) of level n+1 is the chart D(r) of level n”.

Stacks Project, Tag 0EHE (the charts are compatible down the tower). The preimage of the chart D(r̄) of the punctured spectrum of A/t^{n+1}A is the chart D(r̄) of the punctured spectrum of A/tⁿA, for a chart whose basic open lies in the punctured spectrum.

public theorem preimage_levelChart (r : AmbientRing k) (n : ℕ)
    (h : chartOpen k r (n + 1) ≤ levelOpen k (n + 1)) :
    levelOpenMap k n ⁻¹ᵁ levelChart k r (n + 1) = levelChart k r n

Stacks.Algebraization.NonAlgebraizableExample.app_levelSchemeMap_chartOpenEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelTransition.lean, line 151. The attribute's comment: “on D(r) the closed immersion of level schemes induces A_r/t^(n+1) -> A_r/t^n”.

Stacks Project, Tag 0EHE (the closed immersion induces the reduction on chart rings). On the ring of sections over the basic open D(r̄), the closed immersion Spec(A/tⁿA) ⟶ Spec(A/t^{n+1}A) induces the reduction A_r/t^{n+1}A_r → A_r/tⁿA_r.

public theorem app_levelSchemeMap_chartOpenEquiv (r : AmbientRing k) (n : ℕ)
    (w : chartRing k r (n + 1)) :
    ((levelSchemeMap k n).app (chartOpen k r (n + 1))).hom (chartOpenEquiv k r (n + 1) w) =
      chartOpenEquiv k r n (chartReduction k r n w)

Stacks.Algebraization.NonAlgebraizableExample.app_levelOverlapUnit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelTransition.lean, line 257. The attribute's comment: “the closed immersion of punctured spectra carries u at level n+1 to u at level n”.

Stacks Project, Tag 0EHE (the transition units form a tower on the schemes). The closed immersion of the punctured spectrum of A/tⁿA in that of A/t^{n+1}A carries the transition unit of level n + 1 to the transition unit of level n. This is the scheme-level form of Stacks.Algebraization.NonAlgebraizableExample.chartReduction_transitionElement, and the intertwining hypothesis the transition map 𝓛ₙ₊₁ ⟶ 𝓛ₙ is built from.

public theorem app_levelOverlapUnit (a : ℕ → PlaneRing k) (φ : ℕ → ℕ) (n : ℕ) :
    Units.map ((levelOpenMap k n).app (levelOverlap k (n + 1))).hom
        (levelOverlapUnit k a φ (n + 1)) =
      Stacks.SheafOfModules.overlapUnit (levelOverlapUnit k a φ n)
        (levelOpenMap k n ⁻¹ᵁ levelOverlap k (n + 1)) (preimage_levelOverlap k n).le

Stacks.Algebraization.NonAlgebraizableExample.levelTransition, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelTransition.lean, line 278. The attribute's comment: “the transition map L_(n+1) -> L_n of the system”.

Stacks Project, Tag 0EHE (the transition maps of the system). The transition map 𝓛ₙ₊₁ ⟶ 𝓛ₙ of the system of [Stacks, Tag 0EHE], as a morphism from the module of level n + 1 on the punctured spectrum of A/t^{n+1}A to the direct image of the module of level n along the closed immersion of punctured spectra.

public def levelTransition (a : ℕ → PlaneRing k) (φ : ℕ → ℕ) (n : ℕ) :
    levelModule k a φ (n + 1) ⟶
      (Scheme.Modules.pushforward (levelOpenMap k n)).obj (levelModule k a φ n)

Stacks.Algebraization.NonAlgebraizableExample.chartLinearEquiv_levelTransition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableLevelTransition.lean, line 291. The attribute's comment: “in the chart trivializations L_(n+1) -> L_n is the reduction of functions”.

Stacks Project, Tag 0EHE (the transition map in the chart trivializations). Over an open inside one of the two charts, where both modules are trivialized by reading the coordinate of that chart, the transition map is the reduction of functions. This pins levelTransition down.

public theorem chartLinearEquiv_levelTransition (a : ℕ → PlaneRing k) (φ : ℕ → ℕ) (n : ℕ)
    (i : ULift.{u} Bool) {V : (levelOpen k (n + 1)).toScheme.Opens}
    (hV : V ≤ Stacks.SheafOfModules.twoChartFamily
      (levelChart k (xVar k) (n + 1)) (levelChart k (yVar k) (n + 1)) i)
    (hV' : levelOpenMap k n ⁻¹ᵁ V ≤ Stacks.SheafOfModules.twoChartFamily
      (levelChart k (xVar k) n) (levelChart k (yVar k) n) i)
    (s : (Stacks.SheafOfModules.twoChartCocycle
      (levelOverlapUnit k a φ (n + 1))).sectionsSubmodule V) :
    (Stacks.SheafOfModules.twoChartCocycle (levelOverlapUnit k a φ n)).chartLinearEquiv i hV'
        ((levelTransition k a φ n).val.app (op V) s) =
      ((levelOpenMap k n).app V).hom
        ((Stacks.SheafOfModules.twoChartCocycle
          (levelOverlapUnit k a φ (n + 1))).chartLinearEquiv i hV s)

Stacks.Algebraization.NonAlgebraizableExample.isVanishingSectionsParameter_two_pow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableParameter.lean, line 84. The attribute's comment: “a_m = 1 and φ(m) = 2^m satisfy the parameter condition”.

Stacks Project, Tag 0EHE (the first prescribed choice). The coefficients aₘ = 1 and the exponents φ(m) = 2ᵐ satisfy the parameter condition.

public theorem isVanishingSectionsParameter_two_pow {a : ℕ → PlaneRing k} {φ : ℕ → ℕ}
    (ha : ∀ m : ℕ, 2 ≤ m → a m = 1) (hφ : ∀ m : ℕ, 2 ≤ m → φ m = 2 ^ m) :
    IsVanishingSectionsParameter k a φ

Stacks.Algebraization.NonAlgebraizableExample.isVanishingSectionsParameter_sq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableParameter.lean, line 92. The attribute's comment: “a_m = 1 and φ(m) = m^2 satisfy the parameter condition”.

Stacks Project, Tag 0EHE (the second prescribed choice). The coefficients aₘ = 1 and the exponents φ(m) = m² satisfy the parameter condition.

public theorem isVanishingSectionsParameter_sq {a : ℕ → PlaneRing k} {φ : ℕ → ℕ}
    (ha : ∀ m : ℕ, 2 ≤ m → a m = 1) (hφ : ∀ m : ℕ, 2 ≤ m → φ m = m ^ 2) :
    IsVanishingSectionsParameter k a φ

Stacks.Algebraization.NonAlgebraizableExample.sectionsLimit_eq_bot_of_isVanishingSectionsParameter, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableParameter.lean, line 108. The attribute's comment: “lim H^0(U, L_n) = 0 under the parameter condition”.

Stacks Project, Tag 0EHE (the vanishing of the limit of global sections). Under the parameter condition the limit lim H⁰(U, 𝓛ₙ) is zero.

public theorem sectionsLimit_eq_bot_of_isVanishingSectionsParameter (a : ℕ → PlaneRing k)
    (φ : ℕ → ℕ) (h : IsVanishingSectionsParameter k a φ) : sectionsLimit k a φ = ⊥

Stacks.Algebraization.NonAlgebraizableExample.not_exists_compatible_isUnit_mem_gluedSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableParameter.lean, line 120. The attribute's comment: “under the parameter condition (L_n) has no compatible trivializing sections”.

Stacks Project, Tag 0EHE (no compatible trivializing sections under the parameter condition). A trivialization of the glued module 𝓛ₙ is a pair of invertible chart functions matched by the transition element, so a compatible system of trivializations of the whole family would be a system of glued pairs, compatible with reduction modulo tⁿ, whose D(x̄)-components are invertible. Under the parameter condition no such system exists: it would be a nonzero element of lim H⁰(U, 𝓛ₙ), which vanishes. This is the content of the source's second proof of non-algebraizability.

public theorem not_exists_compatible_isUnit_mem_gluedSections (a : ℕ → PlaneRing k) (φ : ℕ → ℕ)
    (h : IsVanishingSectionsParameter k a φ) :
    ¬ ∃ s : (n : ℕ) → chartRing k (xVar k) n × chartRing k (yVar k) n,
      (∀ n : ℕ, s n ∈ gluedSections k n (transitionElement k a φ n)) ∧
      (∀ n : ℕ, (chartReduction k (xVar k) n (s (n + 1)).1,
        chartReduction k (yVar k) n (s (n + 1)).2) = s n) ∧
      ∀ n : ℕ, 0 < n → IsUnit (s n).1

Stacks.Algebraization.NonAlgebraizableExample.uniqueFactorizationMonoid_ambientRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizablePicard.lean, line 64. The attribute's comment: “the ring A = k[x,y][[t]] is a UFD”.

The ambient ring A = k[x,y][[t]] of the example is a unique factorization domain. The polynomial ring k[x,y] is regular and factorial, so its Picard group is trivial, and the power series ring over a regular factorial ring is factorial.

public theorem uniqueFactorizationMonoid_ambientRing :
    UniqueFactorizationMonoid (AmbientRing k)

Stacks.Algebraization.NonAlgebraizableExample.subsingleton_picardGroup_ambientOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizablePicard.lean, line 72. The attribute's comment: “Pic of every open of Spec(k[x,y][[t]]) is trivial”.

Pic of an open of the ambient affine scheme vanishes. The Picard group of every open subscheme of Spec(A), A = k[x,y][[t]], is trivial: A is a unique factorization domain, and [Stacks, Tag 0BDA] trivializes the Picard group of every open of the spectrum of one.

public theorem subsingleton_picardGroup_ambientOpen
    (V : (Spec (CommRingCat.of (AmbientRing k))).Opens) :
    Subsingleton V.toScheme.picardGroup

Stacks.Algebraization.NonAlgebraizableExample.isTrivial_of_isInvertible_ambientOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizablePicard.lean, line 82. The attribute's comment: “an invertible module on an open of Spec(k[x,y][[t]]) is trivial”.

An invertible module on an open of Spec(A) is trivial. An invertible module on an open V ⊆ Spec(k[x,y][[t]]) — for instance on an open V with U ∩ Y ⊆ V ⊆ U on which an algebraizing coherent module becomes invertible — is isomorphic to the structure sheaf of V.

public theorem isTrivial_of_isInvertible_ambientOpen
    {V : (Spec (CommRingCat.of (AmbientRing k))).Opens} (L : V.toScheme.Modules)
    (hL : Stacks.SheafOfModules.IsInvertible V.toScheme.presheaf V.toScheme.ringCatIsSheaf L) :
    Stacks.SheafOfModules.IsTrivial V.toScheme.presheaf V.toScheme.ringCatIsSheaf L

Stacks.Algebraization.NonAlgebraizableExample.sectionsLimitLinearEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableSectionsLimit.lean, line 637. The attribute's comment: “lim H^0(U, L_n) is the module of compatible systems of glued chart pairs”.

Stacks Project, Tag 0EHE (lim H⁰(U, 𝓛ₙ) is the module of compatible glued pairs). The A-module lim H⁰(U, 𝓛ₙ) of the object (𝓛ₙ) of Coh(U, I𝒪_U) is the module sectionsLimit of compatible systems of pairs of chart functions matched by the transition elements: a global section of 𝓛ₙ is read through its functions on the charts D(x̄) and D(ȳ), and the maps of the system become the reductions modulo tⁿ.

public def sectionsLimitLinearEquiv :
    sectionsLimit k a φ ≃ₗ[(situation k).A]
      limitGlobalSections (situation k) (levelCoherentAdicSystem k a φ)

Stacks.Algebraization.NonAlgebraizableExample.nontrivial_limitGlobalSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableSectionsLimit.lean, line 645. The attribute's comment: “lim H^0(U, L_n) is nonzero when a_m = 0 for m ≥ 2”.

Stacks Project, Tag 0EHE (lim H⁰(U, 𝓛ₙ) ≠ 0 for the degenerate choice). When the higher coefficients aₘ vanish, the module lim H⁰(U, 𝓛ₙ) of the system (𝓛ₙ) is nonzero.

public theorem nontrivial_limitGlobalSections (ha : ∀ m : ℕ, 2 ≤ m → a m = 0) :
    Nontrivial (limitGlobalSections (situation k) (levelCoherentAdicSystem k a φ))

Stacks.Algebraization.NonAlgebraizableExample.subsingleton_limitGlobalSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/NonAlgebraizableSectionsLimit.lean, line 655. The attribute's comment: “lim H^0(U, L_n) = 0 for a_m = 1 and φ(m) = 2^m or m^2”.

Stacks Project, Tag 0EHE (lim H⁰(U, 𝓛ₙ) = 0). When every higher coefficient aₘ is 1 and the exponents are φ(m) = 2ᵐ or φ(m) = m², the module lim H⁰(U, 𝓛ₙ) of the system (𝓛ₙ) is zero.

public theorem subsingleton_limitGlobalSections (ha : ∀ m : ℕ, 2 ≤ m → a m = 1)
    (hφ : (∀ m : ℕ, 2 ≤ m → φ m = 2 ^ m) ∨ (∀ m : ℕ, 2 ≤ m → φ m = m ^ 2)) :
    Subsingleton (limitGlobalSections (situation k) (levelCoherentAdicSystem k a φ))

Tag 0EIM, a definition

Tag 0EIM in the Stacks Project.

Stacks.Algebraization.ExtendsToX, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AdicSystemsOnComplement.lean, line 97.

Stacks Project, Tag 0EIM. A coherent I-adic system on U extends to X when it is isomorphic, as an inverse system, to the restriction of a coherent I-adic system on X.

public abbrev ExtendsToX (S : AlgebraizationSituation.{u})
    (F : Stacks.Coherent.CoherentAdicSystems (S.Yι.ker.comap S.U.ι)) : Prop

Tag 0EIN, a lemma

Tag 0EIN in the Stacks Project.

Stacks.Algebraization.extendsToX_iff_pullback_isCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionCriteria/BaseAdicCompletion.lean, line 413.

Stacks Project, Tag 0EIN. A coherent I-adic system on U = Spec(A) ∖ V(𝔞) extends to Spec(A) if and only if its pullback to U' = Spec(A') ∖ V(𝔞'), for A' the I-adic completion of A, is the completion of a coherent 𝒪_{U'}-module.

public theorem extendsToX_iff_pullback_isCompletion (S : AlgebraizationSituation.{u})
    (F : Stacks.Coherent.CoherentAdicSystems (S.Yι.ker.comap S.U.ι)) :
    ExtendsToX S F ↔
      (completionFunctor (completionMap S ⁻¹ᵁ S.U).toScheme
          ((S.Yι.ker.comap S.U.ι).comap (completionMap S ∣_ S.U))).essImage
        ((Stacks.Coherent.coherentAdicPullback (completionMap S ∣_ S.U)
          (S.Yι.ker.comap S.U.ι)).obj F)

Tag 0EHD, an equation

Tag 0EHD in the Stacks Project.

Stacks.Algebraization.limitGlobalSections, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AdicSystemsOnComplement.lean, line 90.

Stacks Project, Tag 0EHD. The A-module M = limₙ H⁰(U, Fₙ) associated to a coherent adic system on U.

public abbrev limitGlobalSections (S : AlgebraizationSituation.{u})
    (F : Stacks.Coherent.CoherentAdicSystems (idealOnOpen S)) : ModuleCat.{u} S.A

Tag 0EIP, a definition

Tag 0EIP in the Stacks Project.

Stacks.Algebraization.CanonicallyExtends, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CanonicalExtension.lean, line 77.

A coherent I-adic system on U canonically extends to X when the quasi-coherent sheaves associated to its global sections are pro-isomorphic to a coherent I-adic system on X.

public abbrev CanonicallyExtends (S : AlgebraizationSituation.{u})
    (F : Stacks.Coherent.CoherentAdicSystems (idealOnOpen S)) : Prop

Tag 0EIR, a lemma

Tag 0EIR in the Stacks Project.

Stacks.Algebraization.isMittagLefflerCategorical_of_canonicallyExtends, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/CanonicalExtensionMittagLeffler.lean, line 178. The attribute's comment: “part (3): the inverse system of global sections of a canonically extending coherent adic system on the open complement satisfies Mittag-Leffler”.

Part (3) of Stacks Project, Tag 0EIR. If a coherent I-adic system on the open complement U canonically extends to X, then the inverse system {H⁰(U, ℱₙ)} of its modules of sections satisfies the Mittag-Leffler condition.

public theorem isMittagLefflerCategorical_of_canonicallyExtends (h : CanonicallyExtends S F) :
    IsMittagLefflerCategorical (globalSectionsSystem S F)

Stacks.Algebraization.limitTopologyAgrees_of_canonicallyExtends, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/CanonicalExtensionMittagLeffler.lean, line 436. The attribute's comment: “part (4), the equality of topologies: the limit topology on M is the I-adic topology, for a canonically extending coherent adic system on the open complement”.

Part (4) of Stacks Project, Tag 0EIR, second half. The limit topology on M = limₙ H⁰(U, ℱₙ) is the I-adic topology.

public theorem limitTopologyAgrees_of_canonicallyExtends (h : CanonicallyExtends S F) :
    LimitTopologyAgrees S F

Stacks.Algebraization.isAdicComplete_and_finite_adicCompletion_of_canonicallyExtends, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/CanonicalExtensionMittagLeffler.lean, line 458. The attribute's comment: “part (4), finiteness: M is finite over the I-adic completion of A, for a canonically extending coherent adic system on the open complement”.

Part (4) of Stacks Project, Tag 0EIR, first half. The module M = limₙ H⁰(U, ℱₙ) is finite over the I-adic completion Â of A: it is I-adically complete, so the canonical map M ⟶ M^ = limₙ M/IⁿM (AdicCompletion.of) is an isomorphism of A-modules, and its completion M^, with its canonical structure of Â-module, is a finite Â-module.

public theorem isAdicComplete_and_finite_adicCompletion_of_canonicallyExtends
    (h : CanonicallyExtends S F) :
    IsAdicComplete S.I (limitGlobalSections S F) ∧
      Module.Finite (AdicCompletion S.I S.A)
        (AdicCompletion S.I (limitGlobalSections S F : Type u))

Stacks.Algebraization.canonicalExtension, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/CanonicalExtensionUniqueness.lean, line 77. The attribute's comment: “unique_extension”.

Stacks Project, Tag 0EIR. A coherent adic system on X extending F, together with a chosen pro-isomorphism from the sheaves associated to the global sections of F.

public noncomputable def canonicalExtension
    (S : AlgebraizationSituation.{u})
    (F : Stacks.Coherent.CoherentAdicSystems (idealOnOpen S))
    (h : CanonicallyExtends S F) :
    Σ G : Stacks.Coherent.CoherentAdicSystems (idealOnX S),
      Stacks.Coherent.diagramToPro (tildeGlobalSectionsSystem S F) ≅
        (Stacks.Coherent.coherentAdicToPro S.X (idealOnX S)).obj G

Stacks.Algebraization.existsUnique_compatibleIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/CanonicalExtensionUniqueness.lean, line 89. The attribute's comment: “unique_extension”.

Stacks Project, Tag 0EIR. Two coherent adic extensions of the same pro-object are isomorphic by exactly one isomorphism compatible with their chosen pro-isomorphisms.

public theorem existsUnique_compatibleIso
    (S : AlgebraizationSituation.{u})
    (P : (Ind (Scheme.QuasicoherentModules S.X)ᵒᵖ)ᵒᵖ)
    (G H : Stacks.Coherent.CoherentAdicSystems (idealOnX S))
    (φ : P ≅ (Stacks.Coherent.coherentAdicToPro S.X (idealOnX S)).obj G)
    (ψ : P ≅ (Stacks.Coherent.coherentAdicToPro S.X (idealOnX S)).obj H) :
    ∃! e : G ≅ H,
      φ ≪≫ (Stacks.Coherent.coherentAdicToPro S.X (idealOnX S)).mapIso e = ψ

Stacks.Algebraization.extendsToX_kerComapSystem_of_canonicallyExtends, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/CanonicalExtensionUniqueness.lean, line 133. The attribute's comment: “part (2): the implication CanonicallyExtends → ExtendsToX, for a coherent adic system on the open complement of an algebraization situation”.

Part (2) of Stacks Project, Tag 0EIR. A coherent I-adic system on the open complement U which canonically extends to X is the restriction to U of a coherent I-adic system on X.

public theorem extendsToX_kerComapSystem_of_canonicallyExtends (h : CanonicallyExtends S F) :
    ExtendsToX S (kerComapSystem S F)

Tag 0EIS, a lemma

Tag 0EIS in the Stacks Project.

Stacks.Algebraization.nonempty_pullback_extension_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CanonicalExtensionBaseChange.lean, line 343. The attribute's comment: “the extension pulls back”.

For A → A' flat, if (G_n) in Coh(X, I 𝒪_X) is pro-isomorphic to (H⁰(U, F_n)^~), then (f^*G_n) is pro-isomorphic to (H⁰(U', F'_n)^~).

public theorem nonempty_pullback_extension_iso
    (G : Stacks.Coherent.CoherentAdicSystems (idealOnX S))
    (e : Stacks.Coherent.diagramToPro (tildeGlobalSectionsSystem S F) ≅
      (Stacks.Coherent.coherentAdicToPro S.X (idealOnX S)).obj G) :
    Nonempty (Stacks.Coherent.diagramToPro
        (tildeGlobalSectionsSystem (S.baseChange A') (baseChangeAdicSystem S A' F)) ≅
      (Stacks.Coherent.coherentAdicToPro (S.baseChange A').X (idealOnX (S.baseChange A'))).obj
        (baseChangeCanonicalExtension S A' G))

Stacks.Algebraization.canonicallyExtends_base_change, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CanonicalExtensionBaseChange.lean, line 364. The attribute's comment: “flat base change of the canonical extension”.

Let S be an algebraization situation: a Noetherian ring A with ideals I ⊆ 𝔞, the affine scheme X = Spec(A) and the open complement U = X ∖ V(𝔞). Let (F_n) be a coherent I-adic system on U and let A → A' be a flat ring map with A' Noetherian. Put X' = Spec(A'), let U' ⊆ X' be the inverse image of U, let g : U' ⟶ U be the induced morphism and set (F'_n) = (g^*F_n). If (F_n) canonically extends to X, then (F'_n) canonically extends to X'.

public theorem canonicallyExtends_base_change (h : CanonicallyExtends S F) :
    CanonicallyExtends (S.baseChange A') (baseChangeAdicSystem S A' F)

Tag 0EHH, a lemma

Tag 0EHH in the Stacks Project.

Stacks.Algebraization.essImage_completionFunctor_of_finite_limit_images, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionCriteria/MittagLefflerAlgebraization.lean, line 84. The attribute's comment: “the in-particular clause, that over an I-adically complete A the system is the completion of a coherent 𝒪_U-module, i.e. lies in the essential image of the completion functor of U, which is condition (2) of 0EIL; deduced from the canonical extension of the main clause by part (2) of 0EIR and the chain of 0EIL”.

The in-particular clause of Stacks Project, Tag 0EHH. In an algebraization situation with A moreover I-adically complete, a coherent I-adic system (ℱₙ) on the open complement U whose global sections have Mittag-Leffler, whose limit topology on M = limₙ H⁰(U, ℱₙ) is the I-adic topology, and whose projections M → H⁰(U, ℱₙ) have finite image, is the completion of a coherent 𝒪_U-module.

The system extends canonically to X by Stacks.Algebraization.canonicallyExtends_of_finite_limit_images, part (2) of Stacks 0EIR turns that into extendability to X, and adic completeness then runs the chain of Stacks 0EIL: an extendable system is the restriction of a completion on X, hence the completion of a module restricted from X, hence a completion on U.

public theorem essImage_completionFunctor_of_finite_limit_images
    (S : AlgebraizationSituation.{u}) [IsAdicComplete S.I S.A]
    (F : Stacks.Coherent.CoherentAdicSystems (idealOnOpen S))
    (hML : IsMittagLefflerCategorical (globalSectionsSystem S F))
    (htop : (⨅ n : ℕ, TopologicalSpace.induced
      (fun x : limitGlobalSections S F =>
        (limit.π (globalSectionsSystem S F) (op n)).hom x) ⊥) =
        S.I.adicModuleTopology (limitGlobalSections S F))
    (hfinite : ∀ n : ℕ, Module.Finite S.A
      (LinearMap.range (limit.π (globalSectionsSystem S F) (op n)).hom)) :
    (completionFunctor S.U.toScheme (idealOnOpen S)).essImage F

Stacks.Algebraization.canonicallyExtends_of_finite_limit_images, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionCriteria/MittagLefflerCriterion.lean, line 1098. The attribute's comment: “canonical extension”.

The Mittag-Leffler, topology, and finite-image hypotheses imply canonical extension of a coherent adic system to X.

public theorem canonicallyExtends_of_finite_limit_images
    (S : Stacks.Algebraization.AlgebraizationSituation.{u})
    (F : Stacks.Coherent.CoherentAdicSystems (Stacks.Algebraization.idealOnOpen S))
    (hML : IsMittagLefflerCategorical (Stacks.Algebraization.globalSectionsSystem S F))
    (htop : (⨅ n : ℕ, TopologicalSpace.induced
      (fun x : Stacks.Algebraization.limitGlobalSections S F =>
        (limit.π (Stacks.Algebraization.globalSectionsSystem S F) (op n)).hom x) ⊥) =
        S.I.adicModuleTopology (Stacks.Algebraization.limitGlobalSections S F))
    (hfinite : ∀ n : ℕ, Module.Finite S.A
      (LinearMap.range (limit.π (Stacks.Algebraization.globalSectionsSystem S F) (op n)).hom)) :
    Stacks.Algebraization.CanonicallyExtends S F

Tag 0DXW, a lemma

Tag 0DXW in the Stacks Project.

Stacks.Algebraization.canonicallyExtends_and_isCompletion_of_principal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionCriteria/PrincipalEquivalence.lean, line 389.

[Stacks, Tag 0DXW]. Let S be the standing situation of [Stacks, Tag 0EHC] and let (F_n) be an object of Coh(U, I𝒪_U). Assume

1. I = (f) is principal with f a nonzerodivisor of A,
2. every F_n is a finite locally free 𝒪_U/Iⁿ𝒪_U-module, and
3. H¹_𝔞(A/fA) and H²_𝔞(A/fA) are finite A-modules.

Then (F_n) extends canonically to X = Spec(A); and if moreover A is f-adically complete, (F_n) is the completion of a coherent 𝒪_U-module.

Hypothesis (2) is used at the stalks, where a finite locally free 𝒪_U/Iⁿ𝒪_U-module is a finite free module over the local ring modulo the n-th power of the stalk of I𝒪_U; that is Stacks.Algebraization.HasFiniteFreeStalks.

The three conditions (a), (b), (c) of the Mittag-Leffler criterion [Stacks, Tag 0EHH] come from Stacks.Algebraization.canonicallyExtends_of_principal_shortExactSequences, whose two hypotheses are discharged here: the short exact sequences 0 → F_n → F_{n+1} → F_1 → 0 by Stacks.Algebraization.hasPrincipalShortExactSequences_of_nonzerodivisor, and the finiteness of H⁰(U, F₁) and H¹(U, F₁) by Stacks.Algebraization.finite_openCohomology_of_hasFiniteFreeStalks. The second clause follows from the first along the chain of [Stacks, Tag 0EIL].

theorem canonicallyExtends_and_isCompletion_of_principal
    (F : Stacks.Coherent.CoherentAdicSystems (idealOnOpen S)) {f : S.A}
    (hI : S.I = Ideal.span {f}) (hnzd : f ∈ nonZeroDivisors S.A)
    (hH1 : Module.Finite S.A (specialFibreLocalCohomology S f 1))
    (hH2 : Module.Finite S.A (specialFibreLocalCohomology S f 2))
    (hfree : HasFiniteFreeStalks S F) :
    CanonicallyExtends S F ∧
      (IsAdicComplete (Ideal.span {f}) S.A →
        (completionFunctor S.U.toScheme (S.Yι.ker.comap S.U.ι)).essImage
          (kerComapSystem S F))

Stacks.Algebraization.canonicallyExtends_of_principal_shortExactSequences, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionCriteria/PrincipalNonzerodivisor.lean, line 511. The attribute's comment: “first clause (canonical extension) only; conditions (a), (b), (c) of 0EHH are proved, but hypotheses (2) and (3) of the source are replaced by the consequences its proof draws from them, namely the short exact sequences 0 → Fₙ → F₍ₙ₊₁₎ → F₁ → 0 and the finiteness of H⁰(U, F₁) and H¹(U, F₁)”.

Stacks Project, Tag 0DXW, first clause. Let S be an algebraization situation whose ideal I is the principal ideal generated by f ∈ A, and let (F_n) be a coherent I-adic system on the open complement U. If the system has the short exact sequences 0 → F_n → F_{n+1} → F_1 → 0 of the source's proof, and if H⁰(U, F_1) and H¹(U, F_1) are finite A-modules, then (F_n) extends canonically to X = Spec(A).

The three hypotheses (a), (b), (c) of the Mittag-Leffler criterion Stacks 0EHH are proved here: (b) from the degree-zero half of Stacks 0EHA, (a) from Stacks 0BLC, and (c) by the source's induction on the short exact sequences.

The source's hypotheses (2) and (3) are replaced by the two consequences its proof uses. Finite local freeness of F_n over 𝒪_U/f^n𝒪_U and the nonzerodivisor property of f are used only to produce the short exact sequences 0 → F_n → F_{n+1} → F_1 → 0, which is the hypothesis h; and the finiteness of H¹_𝔞(A/fA) and H²_𝔞(A/fA) is used only to produce the finiteness of H⁰(U, F_1) and H¹(U, F_1), by Local Cohomology 0BK0 and 0BLT, which are the hypotheses h0 and h1. Neither derivation is carried out here.

The source's second clause, algebraizability over an I-adically complete A, is Stacks.Algebraization.isCompletionNearClosed_of_principal_shortExactSequences.

Stacks 0DXW itself, with the source's own hypotheses and both of its clauses, is Stacks.Algebraization.canonicallyExtends_and_isCompletion_of_principal, which derives the two hypotheses below from them.

theorem canonicallyExtends_of_principal_shortExactSequences (f : S.A)
    (hI : S.I = Ideal.span {f}) (h : HasPrincipalShortExactSequences S F f)
    (h0 : Module.Finite S.A ((globalSectionsSystem S F).obj (op 0)))
    (h1 : Module.Finite S.A ((openCohomologyFunctor S 1).obj (systemObj S F 0))) :
    CanonicallyExtends S F

Stacks.Algebraization.canonicallyExtends_and_isCompletion_of_principal_nonzerodivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionCriteria/PrincipalNonzerodivisorWhole.lean, line 200. The attribute's comment: “both clauses under the source's own conditions (1), (2) and (3): for I = (f) generated by a nonzerodivisor, with every term finite locally free over the infinitesimal neighbourhood it is annihilated by, and with H¹_𝔞(A/fA) and H²_𝔞(A/fA) finite, the system extends canonically to X, and over an I-adically complete A it is the completion of a coherent O_U-module”.

Stacks Project, Tag 0DXW. Let S be an algebraization situation and let (F_n) be a coherent I-adic system on the open complement U. Assume

1. I = (f) is generated by a nonzerodivisor f ∈ 𝔞,
2. every term of the system is finite locally free over the infinitesimal neighbourhood it is annihilated by,
3. H¹_𝔞(A/fA) and H²_𝔞(A/fA) are finite A-modules.

Then (F_n) extends canonically to X = Spec(A), and if A is I-adically complete then (F_n) is the completion of a coherent 𝒪_U-module.

Conditions (1) and (2) give the short exact sequences 0 → F_n → F_{n+1} → F_1 → 0 of the source's proof (Stacks.Algebraization.hasPrincipalShortExactSequences_of_locallyFree), and all three give the finiteness of H⁰(U, F_1) and H¹(U, F_1) (Stacks.Algebraization.finite_complementCohomologyBase_firstTerm). The Mittag-Leffler criterion Stacks 0EHH turns those into the first clause (Stacks.Algebraization.canonicallyExtends_of_principal_shortExactSequences) and the chain of Stacks 0EIL into the second (Stacks.Algebraization.isCompletionNearClosed_of_principal_shortExactSequences).

theorem canonicallyExtends_and_isCompletion_of_principal_nonzerodivisor
    (S : AlgebraizationSituation.{u})
    (F : Stacks.Coherent.CoherentAdicSystems (idealOnOpen S)) (f : S.A)
    (hI : S.I = Ideal.span {f}) (hf : f ∈ nonZeroDivisors S.A)
    (hfree : IsFiniteLocallyFreeAdic (idealOnOpen S) F)
    (h₁ : Module.Finite S.A (localCohomologyBaseQuotient S f 1))
    (h₂ : Module.Finite S.A (localCohomologyBaseQuotient S f 2)) :
    CanonicallyExtends S F ∧
      (IsAdicComplete (Ideal.span {f}) S.A →
        (completionFunctor S.U.toScheme (S.Yι.ker.comap S.U.ι)).essImage (kerComapSystem S F))

Tag 0EHI, a remark

Tag 0EHI in the Stacks Project.

Stacks.LocalCohomology.finite_localCohomology_quotient_span_iff_two_lt_depth_add_height, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/PrincipalQuotientFiniteness.lean, line 415.

Stacks Project, Tag 0EHI. In Situation 0EHC, let I = (f) be principal for a nonzerodivisor f ∈ 𝔞, as in Tag 0DXW. The remark has three assertions, conjoined here into one statement because they are one remark; the first is quantified over the dualizing complexes of A, and the other two carry the remark's own hypotheses as antecedents, exactly as the source states them.

• The parenthetical: if A has a dualizing complex, then A is universally catenary and the formal fibres of its local rings are Cohen--Macaulay. (Tags 0A80, 0A7G, 0AWY.)

• The equivalence: if A is universally catenary with Cohen--Macaulay formal fibres, then H¹_𝔞(A/fA) and H²_𝔞(A/fA) are finite A-modules if and only if

  depth((A/f)_𝔭) + dim((A/𝔭)_𝔮) > 2

for all 𝔭 ∈ V(f) \ V(𝔞) and 𝔮 ∈ V(𝔭) ∩ V(𝔞). This is the Local Cohomology Theorem 0BJV at the cutoff s_{A,𝔞}(A/fA) of Tag 0BJR: the displayed inequality says exactly that the cutoff exceeds 2, the pairs with 𝔭 ∉ V(f) contributing nothing because (A/fA)_𝔭 vanishes there.

• The example: if moreover A/fA satisfies Serre's condition (S₂) and every irreducible component of Z = V(𝔞) has codimension at least 3 in Y = Spec(A/fA), then H¹_𝔞(A/fA) and H²_𝔞(A/fA) are finite.

The two cohomology modules are the local cohomology of A/fA with support in V(𝔞), in the spelling Tag 0BJV uses. depth((A/f)_𝔭) and dim((A/𝔭)_𝔮) are spelled as in the cutoff of Tag 0BJR, namely as Module.depth of (A/fA)_𝔭 over A_𝔭 and as the height of the image of 𝔮 in A/𝔭. The irreducible components of Z are the minimal primes of 𝔞, and the codimension in Y of the component cut out by such a prime 𝔷 is the height of the image of 𝔷 in A/fA.

The two hypotheses _hfa : f ∈ 𝔞 and _hf : f ∈ nonZeroDivisors A are the situation the source places the remark in — Tag 0DXW's I = (f) principal, generated by a nonzerodivisor of 𝔞. They are recorded so the statement has the source's scope and no more; the argument itself never uses them, which is why they are underscored.

public theorem finite_localCohomology_quotient_span_iff_two_lt_depth_add_height
    (A : Type u) [CommRing A] [IsNoetherianRing A] (a : Ideal A) (f : A) (_hfa : f ∈ a)
    (_hf : f ∈ nonZeroDivisors A) :
    (∀ K : DerivedCategory (ModuleCat.{u} A), Dualizing.IsDualizingComplex K →
        Ring.IsUniversallyCatenary A ∧
          ∀ p : PrimeSpectrum A,
            FormalFibersAreCohenMacaulay (Localization.AtPrime p.asIdeal)) ∧
      (Ring.IsUniversallyCatenary A →
        (∀ p : PrimeSpectrum A,
            FormalFibersAreCohenMacaulay (Localization.AtPrime p.asIdeal)) →
        ((Module.Finite A
              (localCohomologyWithSupportIn.{u, u} A (PrimeSpectrum.zeroLocus (a : Set A))
                ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
                  (ModuleCat.of A (A ⧸ Ideal.span {f}))) 1) ∧
            Module.Finite A
              (localCohomologyWithSupportIn.{u, u} A (PrimeSpectrum.zeroLocus (a : Set A))
                ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
                  (ModuleCat.of A (A ⧸ Ideal.span {f}))) 2) ↔
            ∀ p q : PrimeSpectrum A, f ∈ p.asIdeal → ¬ a ≤ p.asIdeal → a ≤ q.asIdeal →
              p.asIdeal ≤ q.asIdeal →
                2 < Module.depth (Localization.AtPrime p.asIdeal)
                      (maximalIdeal (Localization.AtPrime p.asIdeal))
                      (LocalizedModule p.asIdeal.primeCompl (A ⧸ Ideal.span {f})) +
                    (q.asIdeal.map (Ideal.Quotient.mk p.asIdeal)).height) ∧
          (PropertySkRing (A ⧸ Ideal.span {f}) 2 →
            (∀ z ∈ a.minimalPrimes,
              3 ≤ (z.map (Ideal.Quotient.mk (Ideal.span {f}))).height) →
            Module.Finite A
                (localCohomologyWithSupportIn.{u, u} A (PrimeSpectrum.zeroLocus (a : Set A))
                  ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
                    (ModuleCat.of A (A ⧸ Ideal.span {f}))) 1) ∧
              Module.Finite A
                (localCohomologyWithSupportIn.{u, u} A (PrimeSpectrum.zeroLocus (a : Set A))
                  ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
                    (ModuleCat.of A (A ⧸ Ideal.span {f}))) 2))))

Sources

• Section 52.16, Tag 0DXS
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Algebraization.AlgebraizationSituation · Stacks.Algebraization.AlgebraizationSituation.X · Stacks.Algebraization.AlgebraizationSituation.Y · Stacks.Algebraization.AlgebraizationSituation.Z · Stacks.Algebraization.AlgebraizationSituation.U · Stacks.Algebraization.restrictedTildeSystem_isCoherentAdicSystem · Stacks.Algebraization.exists_finiteModuleModel · Stacks.Algebraization.completionFunctor

Section52.17 Algebraization of coherent formal modules, II#

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

Tag 0EIU, a lemma

Tag 0EIU in the Stacks Project.

Stacks.Algebraization.isCompletion_iff_isCompletion_of_isKernelCokernelAnnihilatedByPower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionCriteria/AnnihilatedComparison.lean, line 274. The attribute's comment: “part (2): membership in the essential image of the completion functor”.

Stacks 0EIU part (2). In Situation 0EHC, let α : (F_n) ⟶ (F'_n) be a morphism of Coh(U, I𝒪_U) whose levelwise kernels and cokernels are annihilated by a power of I𝒪_U. Then (F_n) is the completion of a coherent 𝒪_U-module if and only if (F'_n) is.

This is Stacks.Algebraization.essImage_iff_essImage_of_isKernelCokernelAnnihilatedByPower on the open subscheme U, which is Noetherian because X is.

public theorem isCompletion_iff_isCompletion_of_isKernelCokernelAnnihilatedByPower
    (S : AlgebraizationSituation.{u})
    {F G : Stacks.Coherent.CoherentAdicSystems (S.Yι.ker.comap S.U.ι)} (α : F ⟶ G)
    (hα : IsKernelCokernelAnnihilatedByPower (S.Yι.ker.comap S.U.ι) α.hom) :
    (completionFunctor S.U.toScheme (S.Yι.ker.comap S.U.ι)).essImage F ↔
      (completionFunctor S.U.toScheme (S.Yι.ker.comap S.U.ι)).essImage G

Stacks.Algebraization.extendsToX_iff_extendsToX_of_isKernelCokernelAnnihilatedByPower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionCriteria/AnnihilatedComparison.lean, line 297. The attribute's comment: “part (1): extendability to the whole of X”.

Stacks 0EIU part (1). In Situation 0EHC, let α : (F_n) ⟶ (F'_n) be a morphism of Coh(U, I𝒪_U) whose levelwise kernels and cokernels are annihilated by a power of I𝒪_U. Then (F_n) extends to X if and only if (F'_n) does.

Stacks 0EIN, in the form Stacks.Algebraization.extendsToX_iff_pullback_isCompletion, replaces extendability to X by membership in the essential image of the completion functor on the preimage U' of U in the spectrum of the I-adic completion of the base. The pullback along that flat morphism carries α to a morphism of Coh(U', I𝒪_{U'}) whose levelwise kernels and cokernels are still annihilated by a power of the ideal, by Stacks.Coherent.isKernelCokernelAnnihilatedByPower_coherentAdicPullback_map, so Stacks.Algebraization.essImage_iff_essImage_of_isKernelCokernelAnnihilatedByPower applies on U'. The flatness of the completion map is AdicCompletion.flat_of_isNoetherian read through AlgebraicGeometry.Flat.SpecMap_iff, in the form in which the restriction to the open U inherits it.

public theorem extendsToX_iff_extendsToX_of_isKernelCokernelAnnihilatedByPower
    (S : AlgebraizationSituation.{u})
    {F G : Stacks.Coherent.CoherentAdicSystems (S.Yι.ker.comap S.U.ι)} (α : F ⟶ G)
    (hα : IsKernelCokernelAnnihilatedByPower (S.Yι.ker.comap S.U.ι) α.hom) :
    ExtendsToX S F ↔ ExtendsToX S G

Tag 0EHF, a lemma

Tag 0EHF in the Stacks Project.

Stacks.Algebraization.epi_canonicalComparison_of_mittagLeffler, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionCriteria/MittagLefflerCriterion.lean, line 714.

Stacks Project, Tag 0EHF. If the inverse system H⁰(U, F_n) is Mittag-Leffler, every canonical comparison map (M / Iⁿ⁺¹M)^~|_U ⟶ F_n is surjective.

public theorem epi_canonicalComparison_of_mittagLeffler
    (hML : IsMittagLefflerCategorical (globalSectionsSystem S F)) (n : ℕ) :
    Epi (canonicalComparison S F n).1

Tag 0EHG, a lemma

Tag 0EHG in the Stacks Project.

Stacks.Algebraization.limitQuotientSheaves_isCoherentAdicSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionCriteria/LimitQuotientComparison.lean, line 261. The attribute's comment: “coherent inverse system”.

Stacks Project, Tag 0EHG (1). If the limit topology on M = limₙ H⁰(U, F_n) agrees with its I-adic topology, then the restrictions G_n|_U = (M/Iⁿ⁺¹M)^~|_U form a coherent I-adic system on U. In particular every G_n|_U is a coherent 𝒪_U-module.

public theorem limitQuotientSheaves_isCoherentAdicSystem (h : LimitTopologyAgrees S F) :
    Stacks.Coherent.IsCoherentAdicSystem (idealOnOpen S) (limitQuotientSheaves S F)

Stacks.Algebraization.comparison_hom_app_limitSection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionCriteria/LimitQuotientComparison.lean, line 336. The attribute's comment: “canonical comparison”.

Stacks Project, Tag 0EHG (the comparison is the canonical one). On sections over U, the comparison sends the section of G_n|_U induced by an element m of the inverse limit M = limₙ H⁰(U, F_n) to the n-th projection of m.

This pins the comparison down: it is the map induced by the limit projections, not an arbitrary morphism of inverse systems. comparison_hom_app records the same fact as the identification of each component with an adjunction transpose.

public theorem comparison_hom_app_limitSection (h : LimitTopologyAgrees S F) (n : ℕ)
    (m : limitGlobalSections S F) :
    (((comparison S F h).hom.app (op n)).app ⊤) (limitSection S F n m) =
      (limit.π (globalSectionsSystem S F) (op n)).hom m

Stacks.Algebraization.mono_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionCriteria/LimitQuotientComparison.lean, line 386. The attribute's comment: “injective comparison”.

Stacks Project, Tag 0EHG (2). The canonical comparison (G_n|_U) ⟶ (F_n) is a monomorphism in the abelian category Coh(U, I 𝒪_U).

It is not claimed to be an isomorphism: the comparison need not be surjective without a further hypothesis such as the Mittag-Leffler condition of Stacks 0EHF.

public theorem mono_comparison (h : LimitTopologyAgrees S F) : Mono (comparison S F h)

Sources

• Section 52.17, Tag 0EIT
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Algebraization.isCompletion_iff_isCompletion_of_isKernelCokernelAnnihilatedByPower · Stacks.Algebraization.extendsToX_iff_extendsToX_of_isKernelCokernelAnnihilatedByPower · Stacks.Algebraization.epi_canonicalComparison_of_mittagLeffler · Stacks.Algebraization.limitQuotientSheaves_isCoherentAdicSystem · Stacks.Algebraization.comparison_hom_app_limitSection · Stacks.Algebraization.mono_comparison

Section52.18 A distance function#

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

Tag 0EIX, an equation

Tag 0EIX in the Stacks Project.

Stacks.Algebraization.distanceFunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/DistanceFunction.lean, line 180. The attribute's comment: “the distance function”.

Stacks Project, Tag 0EIX. The distance from a closed subset of a Noetherian scheme. It is the minimum weight of all systems of integral closed subschemes from Z to y, or infinity if there is no system.

public def distanceFunction (Y : Scheme.{u}) [IsNoetherian Y] (Z : Closeds Y)
    (y : Y) : ℕ∞

Stacks.Algebraization.nonempty_distanceSystem_of_connectedComponent_inter, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/DistanceFunction.lean, line 296. The attribute's comment: “existence of a zigzag in a connected component meeting Z”.

In a Noetherian scheme, a point connected to the closed subset Z admits a finite zigzag of integral closed subschemes beginning in Z and ending at that point.

public theorem nonempty_distanceSystem_of_connectedComponent_inter
    (Y : Scheme.{u}) [IsNoetherian Y] (Z : Closeds Y) (y : Y)
    (h : (connectedComponent y ∩ (Z : Set Y)).Nonempty) :
    Nonempty (DistanceSystem Y Z y)

Stacks.Algebraization.distanceFunction_le_two_of_zigzag, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/DistanceZigzagTwo.lean, line 113. The attribute's comment: “a zigzag of weight two”.

Stacks Project, Tag 0EIX. In a Noetherian scheme, if a point z of Z is an immediate specialization of v, v an immediate specialization of w, and w ⤳ c ⤳ y is a strict chain of length two, then δ^Y_Z(y) ≤ 2.

public theorem distanceFunction_le_two_of_zigzag (Y : Scheme.{u}) [IsNoetherian Y]
    (Z : Closeds Y) {z v w c y : Y} (hz : z ∈ (Z : Set Y))
    (hvz : v ⤳ z) (hcovvz : ∀ x, v ⤳ x → x ⤳ z → x = v ∨ x = z)
    (hwv : w ⤳ v) (hcovwv : ∀ x, w ⤳ x → x ⤳ v → x = w ∨ x = v)
    (hwc : w ⤳ c) (hcy : c ⤳ y) (hwc' : w ≠ c) (hcy' : c ≠ y) :
    distanceFunction Y Z y ≤ 2

Tag 0EIY, a lemma

Tag 0EIY in the Stacks Project.

Stacks.Algebraization.exists_max_dimensionFunction_on_closed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/DistanceDimensionFunction.lean, line 58. The attribute's comment: “dimension_function_lower_bound”.

Stacks Project, Tag 0EIY. A dimension function has a maximum on a nonempty closed subset of a Noetherian scheme.

public theorem exists_max_dimensionFunction_on_closed
    (Y : Scheme.{u}) [IsNoetherian Y] (Z : Closeds Y)
    (hZ : (Z : Set Y).Nonempty) (δ : DimensionFunction Y) :
    ∃ m : ℤ, IsGreatest (δ '' (Z : Set Y)) m

Stacks.Algebraization.distanceFunction_ge_dimensionFunction_sub_max, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/DistanceDimensionFunction.lean, line 190. The attribute's comment: “dimension_function_lower_bound”.

Stacks Project, Tag 0EIY. The distance from Z is at least the value of a dimension function minus its maximum value on Z.

public theorem distanceFunction_ge_dimensionFunction_sub_max
    (Y : Scheme.{u}) [IsNoetherian Y] (Z : Closeds Y)
    (δ : DimensionFunction Y) (m : ℤ)
    (hm : IsGreatest (δ '' (Z : Set Y)) m) (y : Y) :
    ((δ y - m).toNat : ℕ∞) ≤ distanceFunction Y Z y

Stacks.Algebraization.distanceFunction_le_closureLocalDimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/DistanceLocalDimension.lean, line 75. The attribute's comment: “le_local_dimension”.

Stacks Project, Tag 0EIY. The distance to Z is at most the local dimension of the closure of y at any specialization z lying in Z.

public theorem distanceFunction_le_closureLocalDimension
    (Y : Scheme.{u}) [IsNoetherian Y] (Z : Closeds Y)
    (y z : Y) (hzy : z ∈ closure {y}) (hzZ : z ∈ (Z : Set Y)) :
    (distanceFunction Y Z y : WithBot ℕ∞) ≤
      Order.coheight (⟨z, hzy⟩ : (closure {y} : Set Y))

Stacks.Algebraization.distanceFunction_closedPoint_eq_coheight, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/DistanceLocalRing.lean, line 97. The attribute's comment: “local_catenary_eq_dimension”.

Stacks Project, Tag 0EIY. The distance from the closed point of a catenary Noetherian local spectrum is the dimension of the closure of the given prime.

public theorem distanceFunction_closedPoint_eq_coheight
    (A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    (hcat : Ring.IsCatenary A) (y : PrimeSpectrum A) :
    distanceFunction (Spec (.of A))
      ⟨{IsLocalRing.closedPoint A}, IsLocalRing.isClosed_singleton_closedPoint A⟩ y =
        Order.coheight y

Stacks.Algebraization.distanceFunction_le_of_isOpenImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/DistanceOpenRestriction.lean, line 121. The attribute's comment: “open_restriction_ge”.

Stacks Project, Tag 0EIY. Restriction to an open subscheme does not decrease the distance from a closed subset.

public theorem distanceFunction_le_of_isOpenImmersion
    {U Y : Scheme.{u}} (j : U ⟶ Y) [IsOpenImmersion j] [IsNoetherian Y]
    (Z : Closeds Y) (x : U) :
    letI : IsNoetherian U :=
      { toIsLocallyNoetherian := isLocallyNoetherian_of_isOpenImmersion j
        toCompactSpace := (j.isOpenEmbedding.isInducing.noetherianSpace).compactSpace }
    distanceFunction Y Z (j x) ≤ distanceFunction U (Z.preimage j.continuous) x

Stacks.Algebraization.distanceFunction_le_add_one_of_isImmediateSpecialization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/DistanceSpecialization.lean, line 196. The attribute's comment: “immediate_specialization_bound”.

Stacks Project, Tag 0EIY. An immediate specialization raises the distance from a closed subset by at most one when passing from the special point to the generic point.

public theorem distanceFunction_le_add_one_of_isImmediateSpecialization
    (Y : Scheme.{u}) [IsNoetherian Y] (Z : Closeds Y)
    (hY : IrreducibleClosedsCodim.IsCatenarySpace Y)
    {y' y : Y} (h : IsImmediateSpecialization y' y) :
    distanceFunction Y Z y' ≤ distanceFunction Y Z y + 1

Stacks.Algebraization.distanceFunction_le_of_zigzag_specializations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/DistanceSpecialization.lean, line 225. The attribute's comment: “zigzag_bound”.

Stacks Project, Tag 0EIY. In a zigzag starting in Z, each immediate leftward specialization increases the possible distance by at most one.

public theorem distanceFunction_le_of_zigzag_specializations
    (Y : Scheme.{u}) [IsNoetherian Y] (Z : Closeds Y)
    (hY : IrreducibleClosedsCodim.IsCatenarySpace Y)
    (k : ℕ) (y : Fin (k + 1) → Y) (y' : Fin k → Y)
    (hzero : y ⟨0, Nat.zero_lt_succ k⟩ ∈ (Z : Set Y))
    (hleft : ∀ i : Fin k, IsImmediateSpecialization (y' i) (y (Fin.castSucc i)))
    (hright : ∀ i : Fin k, y' i ⤳ y (Fin.succ i)) :
    distanceFunction Y Z (y (Fin.last k)) ≤ (k : ℕ∞)

Stacks.Algebraization.distanceFunction_sublevel_stableUnderSpecialization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/DistanceSublevel.lean, line 267. The attribute's comment: “sublevel_specialization_stable”.

Stacks Project, Tag 0EIY. Sublevel sets of the distance from a closed subset of a Noetherian scheme are stable under specialization.

public theorem distanceFunction_sublevel_stableUnderSpecialization
    (Y : Scheme.{u}) [IsNoetherian Y] (Z : Closeds Y) (k : ℕ∞) :
    StableUnderSpecialization {y : Y | distanceFunction Y Z y ≤ k}

Stacks.Algebraization.distanceFunction_eq_zero_iff_mem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/DistanceVanishing.lean, line 78. The attribute's comment: “zero_iff_mem”.

Stacks Project, Tag 0EIY. A point has distance zero from a closed subset precisely when it lies in that subset.

public theorem distanceFunction_eq_zero_iff_mem (Y : Scheme.{u}) [IsNoetherian Y]
    (Z : Closeds Y) (y : Y) :
    distanceFunction Y Z y = 0 ↔ y ∈ (Z : Set Y)

Tag 0EIZ, a lemma

Tag 0EIZ in the Stacks Project.

Stacks.Algebraization.distanceFunction_add_trdeg_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/DistanceFiniteType.lean, line 1075.

Stacks Project, Tag 0EIZ. For a finite type morphism with fibres of dimension at most e, the distance at the image point is at most the distance at the source point plus e minus the residue-field transcendence degree.

public theorem distanceFunction_add_trdeg_le
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsNoetherian Y]
    [LocallyOfFiniteType f] [QuasiCompact f]
    (hY : Scheme.IsUniversallyCatenary Y)
    (I : Y.IdealSheafData) (e : ℕ)
    (he : ∀ y : Y, topologicalKrullDim (f.fiber y) ≤ (e : WithBot ℕ∞))
    (x : X) :
    let : IsNoetherian X :=
      { toIsLocallyNoetherian := LocallyOfFiniteType.isLocallyNoetherian f
        toCompactSpace := QuasiCompact.compactSpace_of_compactSpace f }
    let := (f.residueFieldMap x).hom.toAlgebra
    distanceFunction Y I.support (f x) +
        Cardinal.toENat (Algebra.trdeg (Y.residueField (f x)) (X.residueField x)) ≤
      distanceFunction X (I.comap f).support x + (e : ℕ∞)

Tag 0EJ1, an example

Tag 0EJ1 in the Stacks Project.

Stacks.Algebraization.distanceFunction_eq_topologicalKrullDim_add_curveChainDistance, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/DistanceCurveChain.lean, line 594. The attribute's comment: “A generalization of case (1) is if Y is of finite type over a field and Z = {z} is a closed point. Then δ_Z(y) = δ(y) + t where t is the minimum length of a chain of curves connecting z to a closed point of the closure of {y}.”.

Stacks Project, Tag 0EJ1, closing sentence. Let Y be of finite type over a field and Z = {z} a closed point. Then δ_Z(y) = δ(y) + t, where δ(y) = dim closure {y} is the usual dimension function and t is the minimum length of a chain of curves connecting z to a closed point of closure {y}.

Both sides may be infinite: t = ∞ when no chain of curves exists, which happens exactly when z and y lie in different connected components, and then δ_Z(y) = ∞ as well. The equality is read in WithBot ℕ∞, where dim closure {y} lives.

public theorem distanceFunction_eq_topologicalKrullDim_add_curveChainDistance
    {k : Type u} [Field k] (f : Y ⟶ Spec (CommRingCat.of k))
    [LocallyOfFiniteType f] [QuasiCompact f] (z y : Y) (hz : IsClosed ({z} : Set Y)) :
    let : IsNoetherian Y :=
      { toIsLocallyNoetherian := LocallyOfFiniteType.isLocallyNoetherian f
        toCompactSpace := QuasiCompact.compactSpace_of_compactSpace f }
    ((distanceFunction Y (⟨{z}, hz⟩ : Closeds Y) y : ℕ∞) : WithBot ℕ∞) =
      topologicalKrullDim (closure ({y} : Set Y)) +
        ((curveChainDistance Y z (closure {y}) : ℕ∞) : WithBot ℕ∞)

Stacks.Algebraization.distanceFunction_eq_sub_of_specializes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/DistanceSubvariety.lean, line 106. The attribute's comment: “subvariety_specializes”.

Stacks Project, Tag 0EJ1, case (2b). If y ⤳ ζ, i.e. the subvariety closure {ζ} is contained in closure {y}, the distance from closure {ζ} to y is δ(y) - δ(ζ).

public theorem distanceFunction_eq_sub_of_specializes
    (Y : Scheme.{u}) [IsNoetherian Y] (δ : DimensionFunction Y) (ζ y : Y) (h : y ⤳ ζ) :
    distanceFunction Y (⟨closure {ζ}, isClosed_closure⟩ : Closeds Y) y =
      ((δ y - δ ζ).toNat : ℕ∞)

Stacks.Algebraization.distanceFunction_eq_of_isClosed_of_specializes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/DistanceSubvariety.lean, line 149. The attribute's comment: “closed_point_specializes”.

Stacks Project, Tag 0EJ1, case (1a). If z is a closed point and y ⤳ z, the distance from {z} to y is δ(y).

public theorem distanceFunction_eq_of_isClosed_of_specializes
    (Y : Scheme.{u}) [IsNoetherian Y] (δ : DimensionFunction Y) (z y : Y)
    (hz : IsClosed ({z} : Set Y)) (hz0 : δ z = 0) (h : y ⤳ z) :
    distanceFunction Y (⟨{z}, hz⟩ : Closeds Y) y = ((δ y).toNat : ℕ∞)

Stacks.Algebraization.distanceFunction_eq_one_of_not_specializes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/DistanceSubvariety.lean, line 240. The attribute's comment: “subvariety_codim_small”.

Stacks Project, Tag 0EJ1, case (2c). If ζ does not specialize to y and δ(y) ≤ δ(ζ), the distance from closure {ζ} to y is 1.

public theorem distanceFunction_eq_one_of_not_specializes
    (Y : Scheme.{u}) [IsNoetherian Y] [IrreducibleSpace Y] (δ : DimensionFunction Y) (ζ y : Y)
    (h : ¬ ζ ⤳ y) (hle : δ y ≤ δ ζ) :
    distanceFunction Y (⟨closure {ζ}, isClosed_closure⟩ : Closeds Y) y = 1

Stacks.Algebraization.distanceFunction_eq_sub_add_one_of_not_specializes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/DistanceSubvariety.lean, line 378. The attribute's comment: “subvariety_codim_large”.

Stacks Project, Tag 0EJ1, case (2d). If y does not specialize to ζ and δ(ζ) < δ(y), the distance from closure {ζ} to y is δ(y) - δ(ζ) + 1.

public theorem distanceFunction_eq_sub_add_one_of_not_specializes
    (Y : Scheme.{u}) [IsNoetherian Y] [IrreducibleSpace Y] (δ : DimensionFunction Y) (ζ y : Y)
    (h : ¬ y ⤳ ζ) (hlt : δ ζ < δ y) :
    distanceFunction Y (⟨closure {ζ}, isClosed_closure⟩ : Closeds Y) y =
      ((δ y - δ ζ).toNat : ℕ∞) + 1

Stacks.Algebraization.distanceFunction_eq_add_one_of_not_specializes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/DistanceSubvariety.lean, line 394. The attribute's comment: “closed_point_not_specializes”.

Stacks Project, Tag 0EJ1, case (1b). If z is a closed point and y does not specialize to z, the distance from {z} to y is δ(y) + 1.

public theorem distanceFunction_eq_add_one_of_not_specializes
    (Y : Scheme.{u}) [IsNoetherian Y] [IrreducibleSpace Y] (δ : DimensionFunction Y) (z y : Y)
    (hz : IsClosed ({z} : Set Y)) (hz0 : δ z = 0) (h : ¬ y ⤳ z) :
    distanceFunction Y (⟨{z}, hz⟩ : Closeds Y) y = ((δ y).toNat : ℕ∞) + 1

Stacks.Algebraization.distanceFunction_eq_zero_of_closure_subset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/DistanceVanishing.lean, line 110. The attribute's comment: “subvariety_contains_w”.

Stacks Project, Tag 0EJ1. The distance to a closed subset containing the closure of a point is zero.

public theorem distanceFunction_eq_zero_of_closure_subset
    (Y : Scheme.{u}) [IsNoetherian Y] (Z : Closeds Y) (y : Y)
    (h : closure ({y} : Set Y) ⊆ (Z : Set Y)) :
    distanceFunction Y Z y = 0

Sources

• Section 52.18, Tag 0EIW
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Algebraization.distanceFunction · Stacks.Algebraization.nonempty_distanceSystem_of_connectedComponent_inter · Stacks.Algebraization.distanceFunction_le_two_of_zigzag · Stacks.Algebraization.exists_max_dimensionFunction_on_closed · Stacks.Algebraization.distanceFunction_ge_dimensionFunction_sub_max · Stacks.Algebraization.distanceFunction_le_closureLocalDimension · Stacks.Algebraization.distanceFunction_closedPoint_eq_coheight · Stacks.Algebraization.distanceFunction_le_of_isOpenImmersion

Section52.19 Algebraization of coherent formal modules, III#

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

Tag 0EJ3, a definition

Tag 0EJ3 in the Stacks Project.

Stacks.Algebraization.SatisfiesDepthInequalities, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/DepthInequalities.lean, line 149. The attribute's comment: “the (a, b)-inequalities”.

Stacks Project, Tag 0EJ3. A coherent I-adic system on U satisfies the (a, b)-inequalities when, at every point of U ∩ Y and every prime 𝔭 of the completed local ring not containing I𝒪_{X,y}^∧, the depth of the formal stalk at 𝔭 obeys the bound a strictly if V(𝔭) ∩ V(I𝒪_{X,y}^∧) = {𝔪_y^∧}, and in the remaining case obeys a weakly or else the bound b strictly after adding dim(𝒪_{X,y}^∧/𝔭).

public abbrev SatisfiesDepthInequalities (a b : ℤ) : Prop

Stacks.Algebraization.SatisfiesStrictDepthInequalities, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/DepthInequalities.lean, line 166. The attribute's comment: “the strict (a, b)-inequalities”.

Stacks Project, Tag 0EJ3. A coherent I-adic system on U satisfies the strict (a, b)-inequalities when, at every point of U ∩ Y and every prime 𝔭 of the completed local ring not containing I𝒪_{X,y}^∧, the depth of the formal stalk at 𝔭 exceeds the bound a, or else exceeds the bound b after adding dim(𝒪_{X,y}^∧/𝔭).

public abbrev SatisfiesStrictDepthInequalities (a b : ℤ) : Prop

Tag 0EJ4, a lemma

Tag 0EJ4 in the Stacks Project.

Stacks.Algebraization.satisfiesDepthInequalities_of_annihilated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/DepthInequalitiesBootstrap.lean, line 688. The attribute's comment: “part (1)”.

Stacks Project, Tag 0EJ4 (1). A coherent I-adic system on U annihilated by a fixed power of I satisfies the (a, b)-inequalities for every pair of bounds, since every formal stalk then localizes to zero at a prime outside the adic locus and so has infinite depth.

public theorem satisfiesDepthInequalities_of_annihilated
    (S : AlgebraizationSituation.{u})
    (F : Stacks.Coherent.CoherentAdicSystems (idealOnOpen S))
    (hF : ∃ c : ℕ, ∀ n : ℕ,
      _root_.Stacks.AlgebraicGeometry.IdealPower.idealPowerMultiple (idealOnOpen S) c
        (F.obj.obj (op n)) = ⊥)
    (a b : ℤ) :
    SatisfiesDepthInequalities S F a b

Stacks.Algebraization.satisfiesStrictDepthInequalities_of_succ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/DepthInequalitiesBootstrap.lean, line 748. The attribute's comment: “part (2)”.

Stacks Project, Tag 0EJ4 (2). A coherent I-adic system on U satisfying the (a + 1, b)-inequalities satisfies the strict (a, b)-inequalities: in the case distinguished by the adic closed fibre the weak bound a + 1 already beats a strictly.

public theorem satisfiesStrictDepthInequalities_of_succ
    (S : AlgebraizationSituation.{u})
    (F : Stacks.Coherent.CoherentAdicSystems (idealOnOpen S))
    (a b : ℤ)
    (hF : SatisfiesDepthInequalities S F (a + 1) b) :
    SatisfiesStrictDepthInequalities S F a b

Stacks.Algebraization.satisfiesDepthInequalities_iff_bootstrapSituation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/DepthInequalitiesBootstrap.lean, line 1028. The attribute's comment: “part (3)”.

Stacks Project, Tag 0EJ4 (3). If cd(A, I) ≤ d and A has a dualizing complex, then a coherent I-adic system on U satisfies the (s, s + d)-inequalities exactly when, at every point y of U ∩ Y with δ^Y_Z(y) finite, the completed local ring, the ideal I𝒪_{X,y}^∧, the singleton {𝔪_y^∧}, the formal stalk ℱ_y^∧ and the bounds s - δ^Y_Z(y) and d form a bootstrap situation.

public theorem satisfiesDepthInequalities_iff_bootstrapSituation
    (S : AlgebraizationSituation.{u})
    (F : Stacks.Coherent.CoherentAdicSystems (idealOnOpen S))
    (s d : ℤ)
    (hcd : _root_.Stacks.LocalCohomology.cohomologicalDimension S.A S.I
      (Ideal.fg_of_isNoetherianRing S.I) ≤ d)
    (hdual : ∃ K : DerivedCategory (ModuleCat.{max u v} S.A),
      Dualizing.IsDualizingComplex K) :
    SatisfiesDepthInequalities S F s (s + d) ↔
      ∀ (y : S.U.toScheme) (z : S.Y), S.U.ι.base y = S.Yι.base z →
        S.distanceToZ z ≠ ⊤ →
        ∃ B : BootstrapSituation.{u, u, v},
          B.A = completedLocalRing (idealOnOpen S) y ∧
          HEq B.commRing
            (inferInstance : CommRing (completedLocalRing (idealOnOpen S) y)) ∧
          HEq B.I (completedLocalIdeal (idealOnOpen S) y) ∧
          B.M = completedStalk (idealOnOpen S) F y ∧
          HEq B.addCommGroup
            (inferInstance : AddCommGroup (completedStalk (idealOnOpen S) F y)) ∧
          HEq B.module (inferInstance : Module (completedLocalRing (idealOnOpen S) y)
            (completedStalk (idealOnOpen S) F y)) ∧
          HEq B.T {q : PrimeSpectrum (completedLocalRing (idealOnOpen S) y) |
            q.asIdeal = completedMaximalIdeal (idealOnOpen S) y} ∧
          B.s = s - ((S.distanceToZ z).toNat : ℤ) ∧ B.d = d

Stacks.Algebraization.satisfiesDepthInequalities_of_strict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/DepthInequalitiesBootstrap.lean, line 1283. The attribute's comment: “part (4)”.

Stacks Project, Tag 0EJ4 (4). If cd(A, I) ≤ d and A has a dualizing complex, then the strict (s, s + d)-inequalities imply the ordinary (s, s + d)-inequalities: in the case distinguished by the adic closed fibre the prime is isolated in the adic locus, so dim(𝒪_{X,y}^∧/𝔭) ≤ cd(𝒪_{X,y}^∧, I𝒪_{X,y}^∧) ≤ d and the bound s + d on the sum implies the bound s on the depth alone. The isolated-prime bound used for this is Stacks.LocalCohomology.ringKrullDim_quotient_le_cohomologicalDimension', which discharges the local case of Stacks 0BFR on the completion of 𝒪_{X,y}^∧/𝔭 itself rather than taking it as a hypothesis.

public theorem satisfiesDepthInequalities_of_strict
    (S : AlgebraizationSituation.{u})
    (F : Stacks.Coherent.CoherentAdicSystems (idealOnOpen S))
    (s d : ℤ)
    (hcd : _root_.Stacks.LocalCohomology.cohomologicalDimension S.A S.I
      (Ideal.fg_of_isNoetherianRing S.I) ≤ d)
    (_hdual : ∃ K : DerivedCategory (ModuleCat.{max u v} S.A),
      Dualizing.IsDualizingComplex K)
    (hF : SatisfiesStrictDepthInequalities S F s (s + d)) :
    SatisfiesDepthInequalities S F s (s + d)

Stacks.Algebraization.satisfiesDepthInequalities_elementary_properties, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/DepthInequalitiesBootstrap.lean, line 1411.

Stacks Project, Tag 0EJ4. The four elementary properties of the depth–distance inequalities, as one statement about a coherent I-adic system (ℱₙ) on U in an algebraization situation.

1. If (ℱₙ) is annihilated by a power of I, it satisfies the (a, b)-inequalities for every pair of bounds.
2. If (ℱₙ) satisfies the (a + 1, b)-inequalities, it satisfies the strict (a, b)-inequalities.

If moreover cd(A, I) ≤ d and A has a dualizing complex, then

1. (ℱₙ) satisfies the (s, s + d)-inequalities exactly when, at every point y of U ∩ Y with δ^Y_Z(y) finite, the completed local ring, the ideal I𝒪_{X,y}^∧, the singleton {𝔪_y^∧}, the formal stalk ℱ_y^∧ and the bounds s - δ^Y_Z(y) and d form a bootstrap situation, and
2. the strict (s, s + d)-inequalities imply the ordinary (s, s + d)-inequalities.

Parts (1) and (2) are stated here under no hypothesis beyond the situation itself, exactly as the source states them; the hypotheses cd(A, I) ≤ d and the existence of a dualizing complex are carried only by parts (3) and (4), which is where the source introduces them. The four parts are Stacks.Algebraization.satisfiesDepthInequalities_of_annihilated, Stacks.Algebraization.satisfiesStrictDepthInequalities_of_succ, Stacks.Algebraization.satisfiesDepthInequalities_iff_bootstrapSituation and Stacks.Algebraization.satisfiesDepthInequalities_of_strict.

public theorem satisfiesDepthInequalities_elementary_properties
    (S : AlgebraizationSituation.{u})
    (F : Stacks.Coherent.CoherentAdicSystems (idealOnOpen S)) :
    ((∃ c : ℕ, ∀ n : ℕ,
        _root_.Stacks.AlgebraicGeometry.IdealPower.idealPowerMultiple (idealOnOpen S) c
          (F.obj.obj (op n)) = ⊥) →
      ∀ a b : ℤ, SatisfiesDepthInequalities S F a b) ∧
    (∀ a b : ℤ, SatisfiesDepthInequalities S F (a + 1) b →
      SatisfiesStrictDepthInequalities S F a b) ∧
    (∀ s d : ℤ,
      _root_.Stacks.LocalCohomology.cohomologicalDimension S.A S.I
          (Ideal.fg_of_isNoetherianRing S.I) ≤ d →
      (∃ K : DerivedCategory (ModuleCat.{max u v} S.A), Dualizing.IsDualizingComplex K) →
      (SatisfiesDepthInequalities S F s (s + d) ↔
          ∀ (y : S.U.toScheme) (z : S.Y), S.U.ι.base y = S.Yι.base z →
            S.distanceToZ z ≠ ⊤ →
            ∃ B : BootstrapSituation.{u, u, v},
              B.A = completedLocalRing (idealOnOpen S) y ∧
              HEq B.commRing
                (inferInstance : CommRing (completedLocalRing (idealOnOpen S) y)) ∧
              HEq B.I (completedLocalIdeal (idealOnOpen S) y) ∧
              B.M = completedStalk (idealOnOpen S) F y ∧
              HEq B.addCommGroup
                (inferInstance : AddCommGroup (completedStalk (idealOnOpen S) F y)) ∧
              HEq B.module (inferInstance : Module (completedLocalRing (idealOnOpen S) y)
                (completedStalk (idealOnOpen S) F y)) ∧
              HEq B.T {q : PrimeSpectrum (completedLocalRing (idealOnOpen S) y) |
                q.asIdeal = completedMaximalIdeal (idealOnOpen S) y} ∧
              B.s = s - ((S.distanceToZ z).toNat : ℤ) ∧ B.d = d) ∧
        (SatisfiesStrictDepthInequalities S F s (s + d) →
          SatisfiesDepthInequalities S F s (s + d)))

Tag 0EKW, a lemma

Tag 0EKW in the Stacks Project.

Stacks.Algebraization.satisfiesDepthInequalities_two_three_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/DepthInequalitiesCohomologicalDimensionOne.lean, line 423.

In Situation 0EHC let (ℱ_n) be an object of Coh(U, I𝒪_U). If cd(A, I) = 1, then (ℱ_n) satisfies the (2, 3)-inequalities if and only if depth((ℱ_y^∧)_𝔭) + dim(𝒪_{X,y}^∧/𝔭) + δ^Y_Z(y) > 3 for all y ∈ U ∩ Y and all primes 𝔭 ⊆ 𝒪_{X,y}^∧ with 𝔭 ∉ V(I𝒪_{X,y}^∧).

public theorem satisfiesDepthInequalities_two_three_iff (S : AlgebraizationSituation.{u})
    (F : Stacks.Coherent.CoherentAdicSystems (idealOnOpen S))
    (hcd : Stacks.LocalCohomology.cohomologicalDimension S.A S.I
      (IsNoetherian.noetherian S.I) = 1) :
    SatisfiesDepthInequalities S F 2 3 ↔
      ∀ (y : S.U.toScheme) (z : S.Y), S.U.ι.base y = S.Yι.base z →
        ∀ p : PrimeSpectrum (completedLocalRing (idealOnOpen S) y),
          ¬ completedLocalIdeal (idealOnOpen S) y ≤ p.asIdeal →
          depthAddDimAddDistance S F y z p > ((3 : ℤ) : EInt)

Tag 0EJ5, a lemma

Tag 0EJ5 in the Stacks Project.

Stacks.Algebraization.one_le_depth_stalk_of_mixed_irreducibleComponents, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/StrictDepthMixedComponents.lean, line 136.

Stacks Project, Tag 0EJ5. Let A be a Noetherian ring with ideals I ⊆ 𝔞, write X = Spec(A), Y = V(I), Z = V(𝔞), U = X ∖ Z, and suppose A is I-adically complete, has a dualizing complex, and has cd(A, I) ≤ d with d ≥ 1. Let ℱ be a coherent 𝒪_U-module whose completion along I𝒪_U satisfies the strict (1, 1 + d)-inequalities of [Stacks, Tag 0EJ3]. Let x ∈ U be a point such that the closed fibre \overline{\{x\}} ∩ Y has an irreducible component contained in Z and an irreducible component not contained in Z. Then

depth_{𝒪_{U,x}}(ℱ_x) ≥ 1.

The source states this for x ∈ X; a point of Z never satisfies the hypothesis, its closure lying in Z, and ℱ_x is defined only on U, so x ranges over U.

The components on both sides disconnect the closed fibre once their intersection is removed, so [Stacks, Tag 0EG5] produces a point z of the closed fibre inside Z with dim(𝒪_{\overline{\{x\}}, z}) ≤ d + 1; [Stacks, Tag 02IM] produces an immediate generalization r of z still in the closed fibre but outside Z, whose distance to Z is therefore exactly 1 and whose local dimension is at most d. At the point y ∈ U that r determines the strict inequalities, evaluated at a prime of 𝒪_{U,y}^∧ minimal over the extension of the prime of x, force depth((ℱ_y^∧)_𝔭) ≥ 1; and that depth is depth(ℱ_x), by [Stacks, Tag 0338] and [Stacks, Tag 0EHW].

public theorem one_le_depth_stalk_of_mixed_irreducibleComponents
    (S : AlgebraizationSituation.{u}) [IsAdicComplete S.I S.A]
    (F : AlgebraicGeometry.SheafOfModules.CoherentModules S.U.toScheme.ringCatSheaf)
    (d : ℤ) (hd : 1 ≤ d)
    (K : DerivedCategory (ModuleCat.{u} S.A)) (hK : Dualizing.IsDualizingComplex K)
    (hcd : Stacks.LocalCohomology.cohomologicalDimension S.A S.I
      S.I.fg_of_isNoetherianRing ≤ d)
    (hstrict : SatisfiesStrictDepthInequalities S
      ((completionFunctor S.U.toScheme (idealOnOpen S)).obj F) 1 (1 + d))
    (x : S.U.toScheme)
    (hmixed :
      let W : Set S.Y := S.Yι.base ⁻¹' closure ({S.U.ι.base x} : Set S.X)
      let Z : Set W := {y | S.Yι.base y.1 ∈ Set.range S.Zι.base}
      (∃ C : Set W, C ∈ irreducibleComponents W ∧ C ⊆ Z) ∧
        (∃ C : Set W, C ∈ irreducibleComponents W ∧ ¬ C ⊆ Z)) :
    1 ≤ Module.depth (S.U.toScheme.presheaf.stalk x)
      (IsLocalRing.maximalIdeal (S.U.toScheme.presheaf.stalk x))
      ((stalkModuleFunctor x).obj F.obj)

Tag 0EJ6, a lemma

Tag 0EJ6 in the Stacks Project.

Stacks.Algebraization.isIso_globalToFormalSections_of_satisfiesStrictDepthInequalities, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/StrictDepthRecoverSections.lean, line 431. The attribute's comment: “H^0(U,F) = lim H^0(U,F/I^nF) under the strict (1,1+d)-inequalities and depth two off the formal locus”.

Stacks Project, Tag 0EJ6. Let A be a Noetherian ring with ideals I ⊆ 𝔞, write X = Spec(A), Y = V(I), Z = V(𝔞), U = X ∖ Z, and let ℱ be a coherent 𝒪_U-module and d ≥ 1. Assume

1. A is I-adically complete, has a dualizing complex, and cd(A, I) ≤ d,
2. the completion ℱ^∧ of ℱ along I𝒪_U satisfies the strict (1, 1 + d)-inequalities of [Stacks, Tag 0EJ3], and
3. depth(ℱ_x) ≥ 2 for every x ∈ U with \overline{\{x\}} ∩ Y ⊆ Z.

Then

H⁰(U, ℱ) ⟶ lim H⁰(U, ℱ/Iⁿℱ)

is an isomorphism. That arrow is Stacks.Algebraization.FormalSectionsII.globalToFormalSections, whose n-th component is reduction modulo Iⁿ by Stacks.Algebraization.FormalSectionsII.globalToFormalSections_proj.

[Stacks, Tag 0EIG] supplies the conclusion from conditions (1), (3) and its own condition (2), the dimension bound at the associated points of ℱ; that bound is Stacks.Algebraization.associatedPointsClosureDimensionBound_of_satisfiesStrictDepthInequalities, which is where condition (2) here and [Stacks, Tag 0EJ5] are consumed.

public theorem isIso_globalToFormalSections_of_satisfiesStrictDepthInequalities
    (S : AlgebraizationSituation.{u}) [IsAdicComplete S.I S.A]
    (F : AlgebraicGeometry.SheafOfModules.CoherentModules S.U.toScheme.ringCatSheaf)
    (d : ℤ) (hd : 1 ≤ d)
    (K : DerivedCategory (ModuleCat.{u} S.A)) (hK : Dualizing.IsDualizingComplex K)
    (hcd : cohomologicalDimension S.A S.I S.I.fg_of_isNoetherianRing ≤ d)
    (hstrict : SatisfiesStrictDepthInequalities S
      ((completionFunctor S.U.toScheme (idealOnOpen S)).obj F) 1 (1 + d))
    (hdepth : FormalSectionsII.DepthTwoOffFormalLocus S.A S.I S.a F.obj) :
    IsIso (FormalSectionsII.globalToFormalSections S.A S.I S.a F.obj)

Tag 0EJ7, a lemma

Tag 0EJ7 in the Stacks Project.

Stacks.Algebraization.completionFunctor_map_bijective_of_satisfiesStrictDepthInequalities, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/StrictDepthFullyFaithful.lean, line 336. The attribute's comment: “Hom_U(G,F) = Hom_{Coh(U,IO_U)}(G^∧,F^∧) for every coherent G, under the strict (1,1+d)-inequalities and depth two off the formal locus; 0EJ6 applied to F itself”.

Stacks Project, Tag 0EJ7. Let A be a Noetherian ring with ideals I ⊆ 𝔞, write X = Spec(A), Y = V(I), Z = V(𝔞), U = X ∖ Z, and let ℱ be a coherent 𝒪_U-module and d ≥ 1. Assume

1. A is I-adically complete, has a dualizing complex, and cd(A, I) ≤ d,
2. the completion ℱ^∧ of ℱ along I𝒪_U satisfies the strict (1, 1 + d)-inequalities of [Stacks, Tag 0EJ3], and
3. depth(ℱ_x) ≥ 2 for every x ∈ U with \overline{\{x\}} ∩ Y ⊆ Z.

Then

Hom_U(𝒢, ℱ) ⟶ Hom_{Coh(U, I𝒪_U)}(𝒢^∧, ℱ^∧)

is bijective for every coherent 𝒪_U-module 𝒢. The map is the action on morphisms of the completion functor Stacks.Algebraization.completionFunctor of [Stacks, Tag 0880].

The hypotheses are those of [Stacks, Tag 0EJ6] — Stacks.Algebraization.isIso_globalToFormalSections_of_satisfiesStrictDepthInequalities — and that lemma is what is applied: it gives the theorem on formal functions in degree zero for ℱ, which already forces the conclusion for every coherent 𝒢 by Stacks.Algebraization.completionFunctor_map_bijective_of_isIso_globalToFormalSections. The source instead applies [Stacks, Tag 0EJ6] to SheafHom(𝒢, ℱ), after a transport of conditions (2) and (3) to that module whose details it omits; no such transport is needed here.

public theorem completionFunctor_map_bijective_of_satisfiesStrictDepthInequalities
    (S : AlgebraizationSituation.{u}) [IsAdicComplete S.I S.A]
    (F : AlgebraicGeometry.SheafOfModules.CoherentModules S.U.toScheme.ringCatSheaf)
    (d : ℤ) (hd : 1 ≤ d)
    (K : DerivedCategory (ModuleCat.{u} S.A)) (hK : Dualizing.IsDualizingComplex K)
    (hcd : cohomologicalDimension S.A S.I S.I.fg_of_isNoetherianRing ≤ d)
    (hstrict : SatisfiesStrictDepthInequalities S
      ((completionFunctor S.U.toScheme (idealOnOpen S)).obj F) 1 (1 + d))
    (hdepth : FormalSectionsII.DepthTwoOffFormalLocus S.A S.I S.a F.obj)
    (G : AlgebraicGeometry.SheafOfModules.CoherentModules S.U.toScheme.ringCatSheaf) :
    Function.Bijective ((completionFunctor S.U.toScheme (idealOnOpen S)).map :
      (G ⟶ F) →
        ((completionFunctor S.U.toScheme (idealOnOpen S)).obj G ⟶
          (completionFunctor S.U.toScheme (idealOnOpen S)).obj F))

Tag 0EJ8, a lemma

Tag 0EJ8 in the Stacks Project.

Stacks.Algebraization.existsUnique_completionCompatibleIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/UniqueDepthTwoAlgebraization.lean, line 161. The attribute's comment: “the uniqueness half: two depth-two algebraizations are isomorphic by a unique isomorphism compatible with the identifications of completions”.

The uniqueness half of [Stacks, Tag 0EJ8]. In an algebraization situation, let (ℱ_n) be a coherent I𝒪_U-adic system and let d ≥ 1. Assume

1. A is I-adically complete, has a dualizing complex, and cd(A, I) ≤ d,
2. (ℱ_n) satisfies the strict (1, 1 + d)-inequalities of [Stacks, Tag 0EJ3].

Let 𝒢 and ℋ be coherent 𝒪_U-modules with depth(𝒢_x) ≥ 2 and depth(ℋ_x) ≥ 2 for every x ∈ U with closure {x} ∩ Y ⊆ Z, and let φ : 𝒢^∧ ≅ (ℱ_n) and ψ : ℋ^∧ ≅ (ℱ_n). Then there is a unique isomorphism e : 𝒢 ≅ ℋ with e^∧ ≫ ψ = φ.

Together with the existence half this is the uniqueness of the algebraization asserted by the source: condition (2) of the source, that (ℱ_n) be the completion of a coherent module, is witnessed by φ (or by ψ).

public theorem existsUnique_completionCompatibleIso
    (S : AlgebraizationSituation.{u}) [IsAdicComplete S.I S.A]
    (F : Stacks.Coherent.CoherentAdicSystems (idealOnOpen S))
    (d : ℤ) (hd : 1 ≤ d)
    (K : DerivedCategory (ModuleCat.{u} S.A)) (hK : Dualizing.IsDualizingComplex K)
    (hcd : cohomologicalDimension S.A S.I S.I.fg_of_isNoetherianRing ≤ d)
    (hstrict : SatisfiesStrictDepthInequalities S F 1 (1 + d))
    (G H : AlgebraicGeometry.SheafOfModules.CoherentModules S.U.toScheme.ringCatSheaf)
    (hG : FormalSectionsII.DepthTwoOffFormalLocus S.A S.I S.a G.obj)
    (hH : FormalSectionsII.DepthTwoOffFormalLocus S.A S.I S.a H.obj)
    (φ : (completionFunctor S.U.toScheme (idealOnOpen S)).obj G ≅ F)
    (ψ : (completionFunctor S.U.toScheme (idealOnOpen S)).obj H ≅ F) :
    ∃! e : G ≅ H,
      (completionFunctor S.U.toScheme (idealOnOpen S)).map e.hom ≫ ψ.hom = φ.hom

Stacks.Algebraization.exists_completionIso_depthTwoOffFormalLocus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/UniqueDepthTwoAlgebraization.lean, line 239. The attribute's comment: “the existence half: a depth-two algebraization exists”.

The existence half of [Stacks, Tag 0EJ8]. In an algebraization situation, let (ℱ_n) be a coherent I𝒪_U-adic system and let d ≥ 1. Assume

1. A is I-adically complete, has a dualizing complex, and cd(A, I) ≤ d,
2. (ℱ_n) is the completion of some coherent 𝒪_U-module,
3. (ℱ_n) satisfies the strict (1, 1 + d)-inequalities of [Stacks, Tag 0EJ3].

Then (ℱ_n) is the completion of a coherent 𝒪_U-module ℋ with depth(ℋ_x) ≥ 2 at every x ∈ U whose closure meets Y only inside Z.

These are the source's three conditions: condition (2) is the hypothesis halg, which is the source's "(ℱ_n) is the completion of a coherent module", and the depth-two conclusion is Stacks.Algebraization.FormalSectionsII.DepthTwoOffFormalLocus, the transcription of the source's condition (3) already used by [Stacks, Tag 0EJ7] and by the uniqueness half.

The proof is the source's: the depth-two locus T = {x ∈ U : \overline{\{x\}} ∩ Y ⊆ Z} is stable under specialization, the depth bound Stacks.Algebraization.one_le_depth_stalk_of_isImmediateSpecialization_notMem_depthTwoLocus is the source's second paragraph, and the existence half of [Stacks, Tag 0EI3] then extends the given algebraization 𝒢 to a coherent ℋ of depth at least two along T, by a morphism which is an isomorphism on the stalks off T. Since T misses the support of I𝒪_U, that morphism has an isomorphism for its completion (Stacks.Algebraization.isIso_completionFunctor_map_of_isIso_stalkMap_on_support), so ℋ is again an algebraization of (ℱ_n).

public theorem exists_completionIso_depthTwoOffFormalLocus
    (S : AlgebraizationSituation.{u}) [IsAdicComplete S.I S.A]
    (F : Stacks.Coherent.CoherentAdicSystems (idealOnOpen S))
    (d : ℤ) (hd : 1 ≤ d)
    (K : DerivedCategory (ModuleCat.{u} S.A)) (hK : Dualizing.IsDualizingComplex K)
    (hcd : cohomologicalDimension S.A S.I S.I.fg_of_isNoetherianRing ≤ d)
    (hstrict : SatisfiesStrictDepthInequalities S F 1 (1 + d))
    (halg : ∃ G : AlgebraicGeometry.SheafOfModules.CoherentModules S.U.toScheme.ringCatSheaf,
      Nonempty ((completionFunctor S.U.toScheme (idealOnOpen S)).obj G ≅ F)) :
    ∃ H : AlgebraicGeometry.SheafOfModules.CoherentModules S.U.toScheme.ringCatSheaf,
      Nonempty ((completionFunctor S.U.toScheme (idealOnOpen S)).obj H ≅ F) ∧
        FormalSectionsII.DepthTwoOffFormalLocus S.A S.I S.a H.obj

Stacks.Algebraization.existsUnique_depthTwoAlgebraization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/UniqueDepthTwoAlgebraization.lean, line 298. The attribute's comment: “existence and uniqueness, up to unique isomorphism compatible with the identifications of completions, of the depth-two algebraization”.

Stacks Project, Tag 0EJ8. In an algebraization situation, let (ℱ_n) be a coherent I𝒪_U-adic system, an object of Coh(U, I𝒪_U), and let d ≥ 1. Assume

1. A is I-adically complete, has a dualizing complex, and cd(A, I) ≤ d,
2. (ℱ_n) is the completion of a coherent 𝒪_U-module,
3. (ℱ_n) satisfies the strict (1, 1 + d)-inequalities of [Stacks, Tag 0EJ3].

Then there exists a unique coherent 𝒪_U-module ℋ whose completion is (ℱ_n) such that depth(ℋ_x) ≥ 2 for every x ∈ U with \overline{\{x\}} ∩ Y ⊆ Z.

"Unique" is read in the only sense in which a module "whose completion is (ℱ_n)" can be unique: the module comes with an isomorphism ψ : ℋ^∧ ≅ (ℱ_n), and any other coherent 𝒢 of depth at least two off the formal locus, with any φ : 𝒢^∧ ≅ (ℱ_n), is isomorphic to ℋ by a unique isomorphism e : 𝒢 ≅ ℋ with e^∧ ≫ ψ = φ.

The existence is Stacks.Algebraization.exists_completionIso_depthTwoOffFormalLocus (the source's construction through [Stacks, Tag 0EI3]) and the uniqueness is Stacks.Algebraization.existsUnique_completionCompatibleIso (the source's appeal to the mapping property of [Stacks, Tag 0EJ7]).

public theorem existsUnique_depthTwoAlgebraization
    (S : AlgebraizationSituation.{u}) [IsAdicComplete S.I S.A]
    (F : Stacks.Coherent.CoherentAdicSystems (idealOnOpen S))
    (d : ℤ) (hd : 1 ≤ d)
    (K : DerivedCategory (ModuleCat.{u} S.A)) (hK : Dualizing.IsDualizingComplex K)
    (hcd : cohomologicalDimension S.A S.I S.I.fg_of_isNoetherianRing ≤ d)
    (halg : ∃ G : AlgebraicGeometry.SheafOfModules.CoherentModules S.U.toScheme.ringCatSheaf,
      Nonempty ((completionFunctor S.U.toScheme (idealOnOpen S)).obj G ≅ F))
    (hstrict : SatisfiesStrictDepthInequalities S F 1 (1 + d)) :
    ∃ (H : AlgebraicGeometry.SheafOfModules.CoherentModules S.U.toScheme.ringCatSheaf)
      (ψ : (completionFunctor S.U.toScheme (idealOnOpen S)).obj H ≅ F),
      FormalSectionsII.DepthTwoOffFormalLocus S.A S.I S.a H.obj ∧
      ∀ (G : AlgebraicGeometry.SheafOfModules.CoherentModules S.U.toScheme.ringCatSheaf),
        FormalSectionsII.DepthTwoOffFormalLocus S.A S.I S.a G.obj →
        ∀ φ : (completionFunctor S.U.toScheme (idealOnOpen S)).obj G ≅ F,
          ∃! e : G ≅ H,
            (completionFunctor S.U.toScheme (idealOnOpen S)).map e.hom ≫ ψ.hom = φ.hom

Sources

• Section 52.19, Tag 0EJ2
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Algebraization.SatisfiesDepthInequalities · Stacks.Algebraization.SatisfiesStrictDepthInequalities · Stacks.Algebraization.satisfiesDepthInequalities_of_annihilated · Stacks.Algebraization.satisfiesStrictDepthInequalities_of_succ · Stacks.Algebraization.satisfiesDepthInequalities_iff_bootstrapSituation · Stacks.Algebraization.satisfiesDepthInequalities_of_strict · Stacks.Algebraization.satisfiesDepthInequalities_elementary_properties · Stacks.Algebraization.satisfiesDepthInequalities_two_three_iff

Section52.20 Algebraization of coherent formal modules, IV#

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

Tag 0DXU, a lemma

Tag 0DXU in the Stacks Project.

Stacks.Algebraization.canonicallyExtends_and_isCompletion_of_depthDim, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionCriteria/PrincipalDepthDimensionWhole.lean, line 151.

[Stacks, Tag 0DXU]. In the situation of [Stacks, Tag 0EHC] let (ℱₙ) be an object of Coh(U, I𝒪_U). Assume

1. A is local and 𝔞 = 𝔪 is the maximal ideal,
2. A has a dualizing complex,
3. I = (f) is principal for a nonzerodivisor f,
4. each ℱₙ is finite locally free over 𝒪_U/fⁿ𝒪_U,
5. depth((A/f)_𝔭) + dim(A/𝔭) > 1 for every 𝔭 ∈ V(f) other than 𝔪, and
6. depth(A_𝔭) + dim(A/𝔭) > 3 for every 𝔭 ∉ V(f) with V(𝔭) ∩ V(f) ≠ {𝔪}.

Then (ℱₙ) extends canonically to X = Spec(A); in particular, if A is I-adically complete then (ℱₙ) is the completion of a coherent 𝒪_U-module.

The proof is the source's. Conditions (b) and (c) of the Mittag-Leffler criterion [Stacks, Tag 0EHH] come from hypotheses (3), (4) and (5); condition (a) is the finite length of the image of H¹(U, ℱₙ) ⟶ H¹(U, ℱ₁), which [Stacks, Tag 0BK0] (2) and [Stacks, Tag 0EIR] turn into the finite length of the image of H²_𝔪(Mₙ) ⟶ H²_𝔪(M₁) for Mₙ = H⁰(U, ℱₙ), and which local duality — in the shape that reads a vanishing of Ext back as a vanishing of local cohomology — reduces to the finite length of the image of Ext^{-2}_A(M₁, ω) ⟶ Ext^{-2}_A(Mₙ, ω). That last statement is where hypotheses (2), (4), (5) and (6) are spent, over the localizations A_𝔮 at the primes 𝔮 ∈ V(f) ∖ {𝔪}. The normalized dualizing complex the computation needs is produced from hypothesis (2) by Dualizing.exists_isNormalizedDualizingComplex_shift.

theorem canonicallyExtends_and_isCompletion_of_depthDim
    (S : AlgebraizationSituation.{u}) [IsLocalRing S.A] (ha : S.a = maximalIdeal S.A)
    (omega : DerivedCategory (ModuleCat.{u} S.A))
    (homega : Dualizing.IsDualizingComplex (A := S.A) (K := omega))
    (F : Stacks.Coherent.CoherentAdicSystems (idealOnOpen S)) (f : S.A)
    (hI : S.I = Ideal.span {f}) (hf : f ∈ nonZeroDivisors S.A)
    (hfree : IsFiniteLocallyFreeAdic (idealOnOpen S) F)
    (h5 : DepthDimOnDivisor f) (h6 : DepthDimOffDivisor f) :
    CanonicallyExtends S F ∧
      (IsAdicComplete (Ideal.span {f}) S.A →
        (completionFunctor S.U.toScheme (S.Yι.ker.comap S.U.ι)).essImage
          (kerComapSystem S F))

Stacks.RingTheory.AssociatedPrimes.associatedPrimes_quotient_span_singleton_pow_succ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/AssociatedPrime/NonZeroDivisorPowers.lean, line 138. The attribute's comment: “the step of the proof asserting that the associated primes of A/fⁿA agree with those of A/fA, for f a nonzerodivisor”.

Stacks Project, Tag 0DXU (the associated-primes step). For a nonzerodivisor f of a commutative ring A, the associated primes of A ⧸ fⁿ⁺¹A are those of A ⧸ fA.

theorem associatedPrimes_quotient_span_singleton_pow_succ (hf : f ∈ nonZeroDivisors A) (n : ℕ) :
    associatedPrimes A (A ⧸ Ideal.span {f ^ (n + 1)}) =
      associatedPrimes A (A ⧸ Ideal.span {f})

Stacks.RingTheory.PrincipalDivisorDepth.mem_of_depth_add_ringKrullDim_le_three, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Depth/PrincipalDivisorDepthDimension.lean, line 264. The attribute's comment: “the step of the proof deducing from hypothesis (6) that a prime below a point of V(f) other than the closed point, whose depth plus dimension is at most 3, contains f — the source's 'condition (6) tells us these primes are contained in V(f)'”.

Stacks Project, Tag 0DXU (hypothesis (6) confines the support to V(f)). Let f be an element of a local ring A satisfying hypothesis (6), and let 𝔮 be a prime containing f and different from the maximal ideal. Then every prime 𝔭 ⊆ 𝔮 with depth(A_𝔭) + dim(A/𝔭) ≤ 3 contains f.

This is the source's "condition (6) tells us these primes are contained in V(f)", used twice: for dim(A/𝔮) = 2 with the primes of depth(A_𝔭) + dim((A/𝔭)_𝔮) ≤ 1 supporting H^{-1}(ω^•_{A_𝔮}), and for dim(A/𝔮) = 1 with the primes of depth(A_𝔭) + dim((A/𝔭)_𝔮) ≤ 2 supporting H^{-2}(ω^•_{A_𝔮}). In both cases dim(A/𝔭) = dim((A/𝔭)_𝔮) + dim(A/𝔮), so the two support conditions read depth(A_𝔭) + dim(A/𝔭) ≤ 3, which is the single bound used here; 𝔮 itself is the point of V(𝔭) ∩ V(f) other than 𝔪 that lets (6) apply.

theorem mem_of_depth_add_ringKrullDim_le_three [IsLocalRing A] {f : A}
    (h6 : DepthDimOffDivisor f) {q p : PrimeSpectrum A} (hfq : f ∈ q.asIdeal)
    (hqm : q ≠ closedPoint A) (hpq : p.asIdeal ≤ q.asIdeal)
    (hle : (Module.depth A[p] (maximalIdeal A[p]) A[p] : WithBot ℕ∞) +
        ringKrullDim (A ⧸ p.asIdeal) ≤ 3) :
    f ∈ p.asIdeal

Stacks.RingTheory.PrincipalDivisorDepth.exists_mulPowQuotSMulTop_eq_zero_of_depthDimOffDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Depth/PrincipalDivisorDepthDimension.lean, line 336. The attribute's comment: “the step of the proof concluding, for a finite module whose support hypothesis (6) places in V(f), that multiplication by fⁿ from N/fN to N/f^(n+1)N vanishes for all large n — the source's 'thus the desired vanishing for n large enough', in both the dim(A/q) = 2 and the dim(A/q) = 1 case”.

Stacks Project, Tag 0DXU (the vanishing for n large enough). Let f be an element of a local ring A satisfying hypothesis (6), let 𝔮 be a prime containing f and different from the maximal ideal, and let N be a finite A-module every prime of whose support lies below 𝔮 and has depth(A_𝔭) + dim(A/𝔭) ≤ 3. Then the maps fⁿ : N ⧸ fN → N ⧸ f^{n+1}N vanish for all large n.

This is the conclusion of both of the source's two remaining cases. There N is H^{-1}(ω^•_{A_𝔮}) when dim(A/𝔮) = 2 and H^{-2}(ω^•_{A_𝔮}) when dim(A/𝔮) = 1, each a finite module whose support [Stacks, Tag 0DWZ] describes by a depth-plus-dimension bound; the hypothesis (6) step mem_of_depth_add_ringKrullDim_le_three puts that support inside V(f), which makes f nilpotent on N, and the source's "thus the desired vanishing for n large enough" is the vanishing below.

theorem exists_mulPowQuotSMulTop_eq_zero_of_depthDimOffDivisor [IsLocalRing A] {f : A}
    (h6 : DepthDimOffDivisor f) {q : PrimeSpectrum A} (hfq : f ∈ q.asIdeal)
    (hqm : q ≠ closedPoint A) (N : Type u) [AddCommGroup N] [Module A N] [Module.Finite A N]
    (hsupp : ∀ p ∈ Module.support A N, p.asIdeal ≤ q.asIdeal ∧
      (Module.depth A[p] (maximalIdeal A[p]) A[p] : WithBot ℕ∞) +
        ringKrullDim (A ⧸ p.asIdeal) ≤ 3) :
    ∃ c : ℕ, ∀ n, c ≤ n → mulPowQuotSMulTop f N n = 0

Stacks.RingTheory.PrincipalDivisorDepth.one_le_depth_localization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Depth/PrincipalDivisorDepthDimension.lean, line 416. The attribute's comment: “the step of the proof asserting that A_q has depth at least 1 for a prime q containing the nonzerodivisor f, which is what makes H^0 of the dualizing complex of A_q vanish in the case dim(A/q) = 2”.

Stacks Project, Tag 0DXU (depth(A_𝔮) ≥ 1 because f is a nonzerodivisor). For f a nonzerodivisor of a Noetherian ring A and 𝔮 a prime containing f, the local ring A_𝔮 has depth at least one.

This is the source's "H^0(ω^•_{A_𝔮}) = 0 because depth(A_𝔮) ≥ 1 as f is a nonzerodivisor", the input to the case dim(A/𝔮) = 2: the image of f in A_𝔮 lies in the maximal ideal and is still a nonzerodivisor, so it is a regular sequence of length one, and [Stacks, Tag 090R] gives depth(A_𝔮) = depth(A_𝔮/fA_𝔮) + 1 ≥ 1.

theorem one_le_depth_localization [IsNoetherianRing A] {f : A} (hf : f ∈ nonZeroDivisors A)
    {q : PrimeSpectrum A} (hfq : f ∈ q.asIdeal) :
    1 ≤ Module.depth A[q] (maximalIdeal A[q]) A[q]

Stacks.RingTheory.PrincipalDivisorDepth.two_le_depth_localization_of_depthDimOnDivisor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Depth/PrincipalDivisorDepthDimension.lean, line 443. The attribute's comment: “the step of the proof asserting that A_q has depth at least 2 when dim(A/q) = 1, deduced from hypothesis (5) at q together with f being a nonzerodivisor”.

Stacks Project, Tag 0DXU (depth(A_𝔮) ≥ 2 when dim(A/𝔮) = 1). Let f be a nonzerodivisor of a Noetherian local ring A satisfying hypothesis (5), and let 𝔮 be a prime containing f, different from the maximal ideal, with dim(A/𝔮) = 1. Then A_𝔮 has depth at least two.

This is the source's "if dim(A/𝔮) = 1, then condition (5) combined with the fact that f is a nonzerodivisor insures that A_𝔮 has depth at least 2", which is what makes both H^0(ω^•_{A_𝔮}) and H^{-1}(ω^•_{A_𝔮}) vanish in that case. Hypothesis (5) at 𝔮 reads depth((A/fA)_𝔮) + 1 > 1, so (A/fA)_𝔮 = A_𝔮/fA_𝔮 has depth at least one, and [Stacks, Tag 090R] adds the one coming from the nonzerodivisor f.

theorem two_le_depth_localization_of_depthDimOnDivisor [IsNoetherianRing A] [IsLocalRing A]
    {f : A} (hf : f ∈ nonZeroDivisors A) (h5 : DepthDimOnDivisor f) {q : PrimeSpectrum A}
    (hfq : f ∈ q.asIdeal) (hqm : q ≠ closedPoint A)
    (hdim : ringKrullDim (A ⧸ q.asIdeal) = 1) :
    2 ≤ Module.depth A[q] (maximalIdeal A[q]) A[q]

Tag 0DXV, a remark

Tag 0DXV in the Stacks Project.

Stacks.Algebraization.CompleteNormalDomain.one_lt_depth_quotient_add_ringKrullDim_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/CompleteNormalDomainDepthConditions.lean, line 180. The attribute's comment: “assumption (5) of Lemma 0DXU is satisfied”.

Let (A, 𝔪) be a complete Noetherian normal local domain of dimension at least four and let f ∈ A be nonzero. Then depth((A/f)_𝔭) + dim(A/𝔭) > 1 for every prime 𝔭 containing f other than 𝔪.

theorem one_lt_depth_quotient_add_ringKrullDim_quotient (A : Type u) [CommRing A]
    [IsNoetherianRing A] [IsLocalRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A]
    [IsDomain A] [IsIntegrallyClosed A] (hdim : (4 : WithBot ℕ∞) ≤ ringKrullDim A)
    (f : A) (hf : f ≠ 0) (p : PrimeSpectrum A) (hfp : f ∈ p.asIdeal)
    (hp : p.asIdeal ≠ IsLocalRing.maximalIdeal A) :
    (1 : WithBot ℕ∞) <
      (Module.depth (Localization.AtPrime p.asIdeal)
        (IsLocalRing.maximalIdeal (Localization.AtPrime p.asIdeal))
        (LocalizedModule.AtPrime p.asIdeal (A ⧸ Ideal.span {f})) : WithBot ℕ∞) +
        ringKrullDim (A ⧸ p.asIdeal)

Stacks.Algebraization.CompleteNormalDomain.three_lt_depth_add_ringKrullDim_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/CompleteNormalDomainDepthConditions.lean, line 241. The attribute's comment: “assumption (6) of Lemma 0DXU is satisfied”.

Let (A, 𝔪) be a complete Noetherian normal local domain of dimension at least four and let f ∈ 𝔪. Then depth(A_𝔭) + dim(A/𝔭) > 3 for every prime 𝔭 not containing f whose closure meets V(f) outside the closed point.

theorem three_lt_depth_add_ringKrullDim_quotient (A : Type u) [CommRing A] [IsNoetherianRing A]
    [IsLocalRing A] [IsAdicComplete (IsLocalRing.maximalIdeal A) A] [IsDomain A]
    [IsIntegrallyClosed A] (hdim : (4 : WithBot ℕ∞) ≤ ringKrullDim A)
    (f : A) (hfm : f ∈ IsLocalRing.maximalIdeal A) (p : PrimeSpectrum A)
    (hfp : f ∉ p.asIdeal)
    (hp : ({q : PrimeSpectrum A | p.asIdeal ≤ q.asIdeal} ∩
      {q : PrimeSpectrum A | f ∈ q.asIdeal}) ≠
      {⟨IsLocalRing.maximalIdeal A, (IsLocalRing.maximalIdeal.isMaximal A).isPrime⟩}) :
    (3 : WithBot ℕ∞) <
      (Module.depth (Localization.AtPrime p.asIdeal)
        (IsLocalRing.maximalIdeal (Localization.AtPrime p.asIdeal))
        (Localization.AtPrime p.asIdeal) : WithBot ℕ∞) +
        ringKrullDim (A ⧸ p.asIdeal)

Stacks.Algebraization.CompleteNormalDomain.satisfiesAssumptions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/CompleteNormalDomainDepthConditions.lean, line 319. The attribute's comment: “assumptions (1), (2), (3), (5) and (6) of Lemma 0DXU are satisfied”.

Let (A, 𝔪) be a complete Noetherian normal local domain of dimension at least four and let f ∈ 𝔪 be nonzero. Then the algebraization situation with 𝔞 = 𝔪 and I = (f) satisfies assumptions (1), (2), (3), (5) and (6) of [Stacks, Tag 0DXU]: 𝔞 is the maximal ideal, A has a dualizing complex, I is generated by the nonzerodivisor f, and the two depth-dimension inequalities hold off the closed point.

theorem satisfiesAssumptions (A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    [IsAdicComplete (IsLocalRing.maximalIdeal A) A] [IsDomain A] [IsIntegrallyClosed A]
    (hdim : (4 : WithBot ℕ∞) ≤ ringKrullDim A) (f : A)
    (hfm : f ∈ IsLocalRing.maximalIdeal A) (hf : f ≠ 0) :
    (completeNormalSituation A f hfm).a = IsLocalRing.maximalIdeal A ∧
      (∃ K : DerivedCategory (ModuleCat.{u} A), Dualizing.IsDualizingComplex K) ∧
      ((completeNormalSituation A f hfm).I = Ideal.span {f} ∧ IsSMulRegular A f) ∧
      (∀ p : PrimeSpectrum A, f ∈ p.asIdeal →
        p.asIdeal ≠ IsLocalRing.maximalIdeal A →
        (1 : WithBot ℕ∞) <
          (Module.depth (Localization.AtPrime p.asIdeal)
            (IsLocalRing.maximalIdeal (Localization.AtPrime p.asIdeal))
            (LocalizedModule.AtPrime p.asIdeal (A ⧸ Ideal.span {f})) : WithBot ℕ∞) +
            ringKrullDim (A ⧸ p.asIdeal)) ∧
      (∀ p : PrimeSpectrum A, f ∉ p.asIdeal →
        ({q : PrimeSpectrum A | p.asIdeal ≤ q.asIdeal} ∩
          {q : PrimeSpectrum A | f ∈ q.asIdeal}) ≠
          {⟨IsLocalRing.maximalIdeal A, (IsLocalRing.maximalIdeal.isMaximal A).isPrime⟩} →
        (3 : WithBot ℕ∞) <
          (Module.depth (Localization.AtPrime p.asIdeal)
            (IsLocalRing.maximalIdeal (Localization.AtPrime p.asIdeal))
            (Localization.AtPrime p.asIdeal) : WithBot ℕ∞) +
            ringKrullDim (A ⧸ p.asIdeal))

Tag 0EHK, a lemma

Tag 0EHK in the Stacks Project.

Stacks.Algebraization.exists_matlisDual_approximation_localCohomologySystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/LocalCohomologyMatlisApproximation.lean, line 455. The attribute's comment: “the dualization; the essentially constant Matlis dual model of the local cohomology system, which local duality 0AAK and Matlis duality 08Z9 supply in the source, is an explicit hypothesis”.

Stacks Project, Tag 0EHK. In the situation of Stacks 0EHC, let (M_n) be an inverse system of A-modules as in Stacks 0DXT and let (ℱ_n) be the corresponding object of Coh(U, I𝒪_U). Let d ≥ cd(A, I) and s ≥ 0 be integers, assume that A is local with maximal ideal 𝔪 = 𝔞, that A has a dualizing complex, and that (ℱ_n) satisfies the (s, s + d)-inequalities. Let E be an injective hull of the residue field of A. Then for i ≤ s there is a finite A-module N annihilated by a power of I and, for n ≫ 0, compatible maps H^i_𝔪(M_n) → Hom_A(N, E) whose cokernels have finite length and whose kernels K_n form an inverse system in which the image of K_{n''} → K_{n'} has finite length for n'' ≫ n' ≫ 0.

The existence of an essentially constant Matlis dual model of the local cohomology system is an explicit hypothesis: in the source it is the system of the modules Ext^{-i}_A(M_n, ω_A^∙) for a normalized dualizing complex, identified with the Matlis duals of the local cohomology modules by local duality (Stacks 0AAK) and Matlis duality (Stacks 08Z9). This library proves local duality only objectwise, with no naturality in the module (Dualizing.LocalDuality.nonempty_adicCompletion_ext_linearEquiv_linearMap_localCohomology), and its Matlis biduality isomorphism (Dualizing.isIso_matlisEvaluation_of_isArtinian) assumes A adically complete, so the model cannot be produced here; the essential constancy of that system is the substance of the proof in the source.

public theorem exists_matlisDual_approximation_localCohomologySystem
    (S : AlgebraizationSituation.{u}) [IsLocalRing S.A]
    (M : ℕᵒᵖ ⥤ ModuleCat.{u} S.A) (hM : IsFiniteModuleModel S M) (d s : ℤ)
    (E : Type u) [AddCommGroup E] [Module S.A E]
    (ιE : IsLocalRing.ResidueField S.A →ₗ[S.A] E) [Mono (ModuleCat.ofHom ιE)]
    (hιE : Module.IsInjectiveHull (ModuleCat.ofHom ιE))
    (_hmaximal : IsLocalRing.maximalIdeal S.A = S.a)
    (_hdualizing : ∃ K : DerivedCategory (ModuleCat.{u} S.A), Dualizing.IsDualizingComplex K)
    (_hineq : SatisfiesDepthInequalities S
      (coherentAdicSystemOfFiniteModuleModel S M hM) s (s + d))
    (_hcd : _root_.Stacks.LocalCohomology.cohomologicalDimension S.A S.I
      (Ideal.fg_of_isNoetherianRing S.I) ≤ d)
    (_hs : 0 ≤ s)
    (hmodel : ∀ i : ℤ, i ≤ s → ∃ D : MatlisDualModel S M E i,
      IsEssentiallyConstantModFiniteLength S.A S.I D.G) :
    ∀ i : ℤ, i ≤ s →
      ∃ (N : ModuleCat.{u} S.A) (n₀ : ℕ)
        (φ : ∀ n : ℕ,
          (localCohomologySystem S M i).obj (op (n₀ + n)) →ₗ[S.A] (N →ₗ[S.A] E)),
        Module.Finite S.A N ∧
        (∃ k : ℕ, S.I ^ k • (⊤ : Submodule S.A N) = ⊥) ∧
        (∀ (m n : ℕ) (h : m ≤ n),
          φ m ∘ₗ ((localCohomologySystem S M i).map
            (homOfLE (Nat.add_le_add_left h n₀)).op).hom = φ n) ∧
        (∀ n : ℕ, IsFiniteLength S.A ((N →ₗ[S.A] E) ⧸ LinearMap.range (φ n))) ∧
        (∀ m : ℕ, ∃ k : ℕ, ∀ (n : ℕ) (hmn : m ≤ n), k ≤ n →
          IsFiniteLength S.A
            (Submodule.map ((localCohomologySystem S M i).map
              (homOfLE (Nat.add_le_add_left hmn n₀)).op).hom (LinearMap.ker (φ n))))

Stacks.Algebraization.exists_matlisDual_approximation_localCohomologySystem_of_inequalities, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/LocalCohomologyMatlisApproximationOfInequalities.lean, line 52.

Stacks Project, Tag 0EHK. In the situation of Stacks 0EHC, let (M_n) be an inverse system of A-modules as in Stacks 0DXT and let (ℱ_n) be the corresponding object of Coh(U, I𝒪_U). Let d ≥ cd(A, I) and s ≥ 0 be integers, and assume that A is local with maximal ideal 𝔪 = 𝔞, that A has a dualizing complex, and that (ℱ_n) satisfies the (s, s + d)-inequalities. Let E be an injective hull of the residue field of A. Then for i ≤ s there is a finite A-module N annihilated by a power of I and, for n ≫ 0, compatible maps H^i_𝔪(M_n) → Hom_A(N, E) whose cokernels have finite length and whose kernels K_n form an inverse system in which the image of K_{n''} → K_{n'} has finite length for n'' ≫ n' ≫ 0.

public theorem exists_matlisDual_approximation_localCohomologySystem_of_inequalities
    (S : AlgebraizationSituation.{u}) [IsLocalRing S.A]
    (M : ℕᵒᵖ ⥤ ModuleCat.{u} S.A) (hM : IsFiniteModuleModel S M) (d s : ℤ)
    (E : Type u) [AddCommGroup E] [Module S.A E]
    (ιE : IsLocalRing.ResidueField S.A →ₗ[S.A] E) [Mono (ModuleCat.ofHom ιE)]
    (hιE : Module.IsInjectiveHull (ModuleCat.ofHom ιE))
    (hmaximal : IsLocalRing.maximalIdeal S.A = S.a)
    (hdualizing : ∃ K : DerivedCategory (ModuleCat.{u} S.A), Dualizing.IsDualizingComplex K)
    (hineq : SatisfiesDepthInequalities S
      (coherentAdicSystemOfFiniteModuleModel S M hM) s (s + d))
    (hcd : _root_.Stacks.LocalCohomology.cohomologicalDimension S.A S.I
      (Ideal.fg_of_isNoetherianRing S.I) ≤ d)
    (hs : 0 ≤ s) :
    ∀ i : ℤ, i ≤ s →
      ∃ (N : ModuleCat.{u} S.A) (n₀ : ℕ)
        (φ : ∀ n : ℕ,
          (localCohomologySystem S M i).obj (op (n₀ + n)) →ₗ[S.A] (N →ₗ[S.A] E)),
        Module.Finite S.A N ∧
        (∃ k : ℕ, S.I ^ k • (⊤ : Submodule S.A N) = ⊥) ∧
        (∀ (m n : ℕ) (h : m ≤ n),
          φ m ∘ₗ ((localCohomologySystem S M i).map
            (homOfLE (Nat.add_le_add_left h n₀)).op).hom = φ n) ∧
        (∀ n : ℕ, IsFiniteLength S.A ((N →ₗ[S.A] E) ⧸ LinearMap.range (φ n))) ∧
        (∀ m : ℕ, ∃ k : ℕ, ∀ (n : ℕ) (hmn : m ≤ n), k ≤ n →
          IsFiniteLength S.A
            (Submodule.map ((localCohomologySystem S M i).map
              (homOfLE (Nat.add_le_add_left hmn n₀)).op).hom (LinearMap.ker (φ n))))

Tag 0EJ9, a lemma

Tag 0EJ9 in the Stacks Project.

Stacks.Algebraization.extendsToX_of_isLocalRing_of_eq_span_singleton, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/ExtensionPrincipalLocalTheorem.lean, line 89. The attribute's comment: “first assertion: (ℱₙ) extends to X”.

Stacks Project, Tag 0EJ9. In Situation 0EHC let (ℱₙ) be an object of Coh(U, I𝒪_U). Assume (1) A is local and 𝔞 = 𝔪 is the maximal ideal, (2) A has a dualizing complex, (3) I = (f) is a principal ideal, and (4) (ℱₙ) satisfies the (2, 3)-inequalities. Then (ℱₙ) extends to X.

public theorem extendsToX_of_isLocalRing_of_eq_span_singleton
    (S : AlgebraizationSituation.{u}) [IsLocalRing S.A]
    (F : Stacks.Coherent.CoherentAdicSystems (idealOnOpen S)) (f : S.A)
    (ha : S.a = IsLocalRing.maximalIdeal S.A)
    (hdual : ∃ K : DerivedCategory (ModuleCat.{u} S.A), Dualizing.IsDualizingComplex K)
    (hI : S.I = Ideal.span {f})
    (hineq : SatisfiesDepthInequalities S F 2 3) :
    ExtendsToX S (toKerSystem S F)

Stacks.Algebraization.essImage_completionFunctor_of_isLocalRing_of_eq_span_singleton, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/ExtensionPrincipalLocalTheorem.lean, line 117. The attribute's comment: “in-particular clause: over an I-adically complete A, (ℱₙ) is the completion of a coherent 𝒪_U-module”.

Stacks Project, Tag 0EJ9, in-particular clause. In the situation of Stacks.Algebraization.extendsToX_of_isLocalRing_of_eq_span_singleton, if moreover A is I-adically complete then (ℱₙ) is the completion of a coherent 𝒪_U-module.

The system extends to X, and over an I-adically complete base an extendable system is the restriction of a completion on X, hence the completion of a module restricted from X, hence a completion on U ([Stacks, Tag 0EIL]).

public theorem essImage_completionFunctor_of_isLocalRing_of_eq_span_singleton
    (S : AlgebraizationSituation.{u}) [IsLocalRing S.A] [IsAdicComplete S.I S.A]
    (F : Stacks.Coherent.CoherentAdicSystems (idealOnOpen S)) (f : S.A)
    (ha : S.a = IsLocalRing.maximalIdeal S.A)
    (hdual : ∃ K : DerivedCategory (ModuleCat.{u} S.A), Dualizing.IsDualizingComplex K)
    (hI : S.I = Ideal.span {f})
    (hineq : SatisfiesDepthInequalities S F 2 3) :
    (completionFunctor S.U.toScheme (S.Yι.ker.comap S.U.ι)).essImage (toKerSystem S F)

Tag 0EJA, a lemma

Tag 0EJA in the Stacks Project.

Stacks.Algebraization.two_lt_depth_add_dim_of_satisfiesDepthInequalities, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/DepthInequalitiesUnwinding.lean, line 189. The attribute's comment: “necessity of the depth inequality at the points of U ∩ Y of dimension one”.

Stacks Project, Tag 0EJA. In Situation 0EHC with A local, 𝔞 = 𝔪 and cd(A, I) = 1, if (ℱ_n) satisfies the (2, 3)-inequalities then depth((ℱ_y^∧)_𝔭) + dim(𝒪_{X,y}^∧/𝔭) > 2 for every y ∈ U ∩ Y with dim({y}‾) = 1 and every prime 𝔭 ⊆ 𝒪_{X,y}^∧ not containing I𝒪_{X,y}^∧.

public theorem two_lt_depth_add_dim_of_satisfiesDepthInequalities
    (S : AlgebraizationSituation.{u}) [IsLocalRing S.A]
    (ha : S.a = maximalIdeal S.A)
    (hcd : Stacks.LocalCohomology.cohomologicalDimension S.A S.I
      (IsNoetherian.noetherian S.I) = 1)
    (F : Stacks.Coherent.CoherentAdicSystems (idealOnOpen S))
    (h : SatisfiesDepthInequalities S F 2 3)
    (y : S.U.toScheme) (z : S.Y) (hyz : S.U.ι.base y = S.Yι.base z)
    (hdim : Order.height (S.U.ι.base y) = 1)
    (p : PrimeSpectrum (completedLocalRing (idealOnOpen S) y))
    (hp : ¬ completedLocalIdeal (idealOnOpen S) y ≤ p.asIdeal) :
    enatToEInt (completedStalkDepth (idealOnOpen S) F y p) +
        krullDimToEInt (ringKrullDim (completedLocalRing (idealOnOpen S) y ⧸ p.asIdeal)) >
      ((2 : ℤ) : EInt)

Stacks.Algebraization.satisfiesDepthInequalities_two_three_iff_two_lt_depth_add_dim, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/DepthInequalitiesUnwindingCriterion.lean, line 449. The attribute's comment: “corrected form: the published statement, at hypotheses (1) and (2) alone, is false, by Stacks.NonCatenaryExample.not_stacks0EJA, an example in which A/I is not catenary; this is the equivalence with A/I catenary and the completed local rings of U at the points of U ∩ Y of dimension one universally catenary with Cohen-Macaulay formal fibres”.

In Situation 0EHC let (ℱ_n) be an object of Coh(U, I𝒪_U). Assume A is local with 𝔞 = 𝔪, that cd(A, I) = 1, and that A/I is catenary. Assume also that, at every point y' of U ∩ Y with dim({y'}‾) = 1, the completed local ring 𝒪_{X,y'}^∧ is universally catenary and has Cohen--Macaulay formal fibres. Then (ℱ_n) satisfies the (2, 3)-inequalities if and only if depth((ℱ_y^∧)_𝔭) + dim(𝒪_{X,y}^∧/𝔭) > 2 for every y ∈ U ∩ Y with dim({y}‾) = 1 and every prime 𝔭 ⊆ 𝒪_{X,y}^∧ with 𝔭 ∉ V(I𝒪_{X,y}^∧).

Without the catenarity of A/I and the hypotheses on the completed stalks the statement is false: see Stacks.NonCatenaryExample.not_stacks0EJA.

public theorem satisfiesDepthInequalities_two_three_iff_two_lt_depth_add_dim
    (S : AlgebraizationSituation.{u}) [IsLocalRing S.A]
    (ha : S.a = maximalIdeal S.A)
    (hcat : Ring.IsCatenary (S.A ⧸ S.I))
    (hcatStalk : ∀ (y' : S.U.toScheme) (z' : S.Y), S.U.ι.base y' = S.Yι.base z' →
      Order.height (S.U.ι.base y') = 1 →
      Ring.IsUniversallyCatenary (completedLocalRing (idealOnOpen S) y'))
    (hCMStalk : ∀ (y' : S.U.toScheme) (z' : S.Y), S.U.ι.base y' = S.Yι.base z' →
      Order.height (S.U.ι.base y') = 1 →
      IsPRing Stacks.AdicCompletionFibre.cohenMacaulayRingMapProperty.{u}
        (completedLocalRing (idealOnOpen S) y'))
    (hcd : Stacks.LocalCohomology.cohomologicalDimension S.A S.I
      (IsNoetherian.noetherian S.I) = 1)
    (F : Stacks.Coherent.CoherentAdicSystems (idealOnOpen S)) :
    SatisfiesDepthInequalities S F 2 3 ↔
      ∀ (y : S.U.toScheme) (z : S.Y), S.U.ι.base y = S.Yι.base z →
        Order.height (S.U.ι.base y) = 1 →
        ∀ p : PrimeSpectrum (completedLocalRing (idealOnOpen S) y),
          ¬ completedLocalIdeal (idealOnOpen S) y ≤ p.asIdeal →
          ((2 : ℤ) : EInt) <
            enatToEInt (completedStalkDepth (idealOnOpen S) F y p) +
              krullDimToEInt
                (ringKrullDim (completedLocalRing (idealOnOpen S) y ⧸ p.asIdeal))

Stacks.Algebraization.satisfiesDepthInequalities_two_three_iff_two_lt_depth_add_dim_of_isDualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/DepthInequalitiesUnwindingCriterion.lean, line 522. The attribute's comment: “corrected form: the published statement, at hypotheses (1) and (2) alone, is false, by Stacks.NonCatenaryExample.not_stacks0EJA, an example in which A/I is not catenary; this is the equivalence for A with a dualizing complex, the standing hypothesis of the neighbouring 0EJ9 and 0EJB”.

In Situation 0EHC let (ℱ_n) be an object of Coh(U, I𝒪_U). Assume A is local with 𝔞 = 𝔪, that A has a dualizing complex, and that cd(A, I) = 1. Then (ℱ_n) satisfies the (2, 3)-inequalities if and only if depth((ℱ_y^∧)_𝔭) + dim(𝒪_{X,y}^∧/𝔭) > 2 for every y ∈ U ∩ Y with dim({y}‾) = 1 and every prime 𝔭 ⊆ 𝒪_{X,y}^∧ with 𝔭 ∉ V(I𝒪_{X,y}^∧).

public theorem satisfiesDepthInequalities_two_three_iff_two_lt_depth_add_dim_of_isDualizingComplex
    (S : AlgebraizationSituation.{u}) [IsLocalRing S.A]
    (ha : S.a = maximalIdeal S.A)
    (hdual : ∃ K : DerivedCategory (ModuleCat.{u} S.A), Dualizing.IsDualizingComplex K)
    (hcd : Stacks.LocalCohomology.cohomologicalDimension S.A S.I
      (IsNoetherian.noetherian S.I) = 1)
    (F : Stacks.Coherent.CoherentAdicSystems (idealOnOpen S)) :
    SatisfiesDepthInequalities S F 2 3 ↔
      ∀ (y : S.U.toScheme) (z : S.Y), S.U.ι.base y = S.Yι.base z →
        Order.height (S.U.ι.base y) = 1 →
        ∀ p : PrimeSpectrum (completedLocalRing (idealOnOpen S) y),
          ¬ completedLocalIdeal (idealOnOpen S) y ≤ p.asIdeal →
          ((2 : ℤ) : EInt) <
            enatToEInt (completedStalkDepth (idealOnOpen S) F y p) +
              krullDimToEInt
                (ringKrullDim (completedLocalRing (idealOnOpen S) y ⧸ p.asIdeal))

Stacks.NonCatenaryExample.not_stacks0EJA, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/NonCatenaryCounterexample/Final.lean, line 40. The attribute's comment: “refutation of the published 'if' direction: at hypotheses (1) and (2) alone, the depth inequality at the points of U ∩ Y of dimension one does not imply the (2, 3)-inequalities; in the example A/I is not catenary”.

Stacks 0EJA is false as published. There is an algebraization situation (Situation 0EHC) with A Noetherian local, 𝔞 = 𝔪, cd(A, I) = 1, and an object (ℱₙ) of Coh(U, I𝒪_U) such that depth((ℱ_y^∧)_𝔭) + dim(𝒪_{X,y}^∧/𝔭) > 2 for every y ∈ U ∩ Y with dim({y}‾) = 1 and every 𝔭 ∉ V(I𝒪_{X,y}^∧), but (ℱₙ) does not satisfy the (2, 3)-inequalities.

theorem not_stacks0EJA :
    ¬ ∀ (S : AlgebraizationSituation.{u}) [IsLocalRing S.A], S.a = maximalIdeal S.A →
      Stacks.LocalCohomology.cohomologicalDimension S.A S.I (IsNoetherian.noetherian S.I) = 1 →
      ∀ F : Stacks.Coherent.CoherentAdicSystems (idealOnOpen S),
        (SatisfiesDepthInequalities S F 2 3 ↔
          ∀ (y : S.U.toScheme) (z : S.Y), S.U.ι.base y = S.Yι.base z →
            Order.height (S.U.ι.base y) = 1 →
            ∀ p : PrimeSpectrum (completedLocalRing (idealOnOpen S) y),
              ¬ completedLocalIdeal (idealOnOpen S) y ≤ p.asIdeal →
              ((2 : ℤ) : EInt) <
                enatToEInt (completedStalkDepth (idealOnOpen S) F y p) +
                  krullDimToEInt
                    (ringKrullDim (completedLocalRing (idealOnOpen S) y ⧸ p.asIdeal)))

Tag 0EJB, a lemma

Tag 0EJB in the Stacks Project.

Stacks.Algebraization.satisfiesDepthInequalities_of_finiteLocallyFreeOutside, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/DepthInequalitiesLocallyFreeOutside.lean, line 669.

In Situation 0EHC let (ℱ_n) be an object of Coh(U, I𝒪_U). Assume (1) A is local with 𝔞 = 𝔪, (2) A has a dualizing complex, (3) cd(A, I) = 1, (4) for y ∈ U ∩ Y the module ℱ_y^∧ is finite locally free outside V(I𝒪_{X,y}^∧), and (5) either (a) X \ Y is (S₂) and every irreducible component of X not contained in Y has dimension ≥ 4, or (b) for every prime 𝔭 ∉ V(I) with V(𝔭) ∩ V(I) ≠ {𝔪} one has depth(A_𝔭) + dim(A/𝔭) > 3. Then (ℱ_n) satisfies the (2, 3)-inequalities.

public theorem satisfiesDepthInequalities_of_finiteLocallyFreeOutside
    (S : AlgebraizationSituation.{u}) [IsLocalRing S.A]
    (hmax : S.a = maximalIdeal S.A)
    (hdual : ∃ K : DerivedCategory (ModuleCat.{u} S.A), Dualizing.IsDualizingComplex K)
    (hcd : Stacks.LocalCohomology.cohomologicalDimension S.A S.I
      (IsNoetherian.noetherian S.I) = 1)
    (F : Stacks.Coherent.CoherentAdicSystems (idealOnOpen S))
    (hfree : ∀ (y : S.U.toScheme) (z : S.Y), S.U.ι.base y = S.Yι.base z →
      ∀ p : PrimeSpectrum (completedLocalRing (idealOnOpen S) y),
        ¬ completedLocalIdeal (idealOnOpen S) y ≤ p.asIdeal →
        Module.Free (Localization.AtPrime p.asIdeal)
          (LocalizedModule p.asIdeal.primeCompl (completedStalk (idealOnOpen S) F y)))
    (hcondition :
      ((∀ p : PrimeSpectrum S.A, ¬ S.I ≤ p.asIdeal →
          PropertySkRing (Localization.AtPrime p.asIdeal) 2) ∧
        (∀ p : PrimeSpectrum S.A, IsMinimalPrime p.asIdeal →
          ¬ S.I ≤ p.asIdeal →
          (4 : WithBot ℕ∞) ≤ ringKrullDim (S.A ⧸ p.asIdeal))) ∨
      (∀ p : PrimeSpectrum S.A, ¬ S.I ≤ p.asIdeal →
        ({q : PrimeSpectrum S.A | p.asIdeal ≤ q.asIdeal} ∩
          {q : PrimeSpectrum S.A | S.I ≤ q.asIdeal}) ≠
          {⟨maximalIdeal S.A, (IsLocalRing.maximalIdeal.isMaximal S.A).isPrime⟩} →
        (3 : WithBot ℕ∞) <
          (Module.depth (Localization.AtPrime p.asIdeal)
            (maximalIdeal (Localization.AtPrime p.asIdeal))
            (Localization.AtPrime p.asIdeal) : WithBot ℕ∞) +
            ringKrullDim (S.A ⧸ p.asIdeal))) :
    SatisfiesDepthInequalities S F 2 3

Tag 0EJC, a remark

Tag 0EJC in the Stacks Project.

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

Stacks Project, Tag 0EJC. Let (A, 𝔪) be a Noetherian local ring which has a dualizing complex and is complete with respect to f ∈ 𝔪, let (ℱₙ) be an object of Coh(U, f𝒪_U) where U is the punctured spectrum of A, and set Y = V(f) ⊆ X = Spec(A). If for every y ∈ U ∩ V(f) closed in U, i.e. with dim({y}‾) = 1, the 𝒪_{X,y}^∧-module ℱ_y^∧ satisfies

1. ℱ_y^∧[1/f] is (S₂) as an 𝒪_{X,y}^∧[1/f]-module, and
2. dim(𝒪_{X,y}^∧/𝔭) ≥ 3 for every 𝔭 ∈ Ass(ℱ_y^∧[1/f]),

then (ℱₙ) is the completion of a coherent 𝒪_U-module.

public theorem essImage_completionFunctor_of_hasSerreCompletedStalkConditions
    (S : AlgebraizationSituation.{u}) [IsLocalRing S.A] [IsAdicComplete S.I S.A]
    (F : Stacks.Coherent.CoherentAdicSystems (idealOnOpen S)) (f : S.A)
    (ha : S.a = IsLocalRing.maximalIdeal S.A)
    (hdual : ∃ K : DerivedCategory (ModuleCat.{u} S.A), Dualizing.IsDualizingComplex K)
    (hI : S.I = Ideal.span {f})
    (hserre : ∀ (y : S.U.toScheme) (z : S.Y), S.U.ι.base y = S.Yι.base z →
      Order.height (S.U.ι.base y) = 1 → HasSerreCompletedStalkConditions S F f y) :
    (completionFunctor S.U.toScheme (S.Yι.ker.comap S.U.ι)).essImage (toKerSystem S F)

Sources

• Section 52.20, Tag 0EHJ
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Algebraization.canonicallyExtends_and_isCompletion_of_depthDim · Stacks.RingTheory.AssociatedPrimes.associatedPrimes_quotient_span_singleton_pow_succ · Stacks.RingTheory.PrincipalDivisorDepth.mem_of_depth_add_ringKrullDim_le_three · Stacks.RingTheory.PrincipalDivisorDepth.exists_mulPowQuotSMulTop_eq_zero_of_depthDimOffDivisor · Stacks.RingTheory.PrincipalDivisorDepth.one_le_depth_localization · Stacks.RingTheory.PrincipalDivisorDepth.two_le_depth_localization_of_depthDimOnDivisor · Stacks.Algebraization.CompleteNormalDomain.one_lt_depth_quotient_add_ringKrullDim_quotient · Stacks.Algebraization.CompleteNormalDomain.three_lt_depth_add_ringKrullDim_quotient

Section52.21 Improving coherent formal modules#

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

Tag 0EJE, a lemma

Tag 0EJE in the Stacks Project.

Stacks.Algebraization.finite_completedStalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/CompletedStalkFinite.lean, line 441. The attribute's comment: “finiteness of the completed stalk over the completed local ring”.

Stacks 0EJE, finiteness of the completed stalk.

Let ℐ be a quasi-coherent sheaf of ideals on a locally Noetherian scheme X and let (ℱ_n) be an object of Coh(X, ℐ). At every point x the completed stalk ℱ_x^∧ is a finite module over the completed local ring 𝒪_{X,x}^∧.

Each ℱ_n is coherent, so ℱ_{n,x} is a finite 𝒪_{X,x}-module, and the transitions are surjective on stalks with kernel ℐ_x^{n+1} ℱ_{n+1,x}; the limit therefore has reduction ℱ_{0,x} modulo ℐ_x, which is finite, and [Stacks, Tag 031D] turns a module with finite reduction into one whose ℐ_x-adic completion is finite over 𝒪_{X,x}^∧.

theorem finite_completedStalk [IsLocallyNoetherian X] (J : X.IdealSheafData)
    (G : Stacks.Coherent.CoherentAdicSystems J) (x : X) :
    Module.Finite (completedLocalRing J x) (completedStalk J G x)

Stacks.Algebraization.isDepthOneQuotient_toImprovedSystem_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/ImprovingFormalModules.lean, line 112. The attribute's comment: “the canonical map (ℱₙ) → (ℱ'ₙ) of inverse systems of coherent modules, and its property (1); properties (2) and (3), which identify (ℱ'ₙ) pro-isomorphically with an object of Coh(X, ℐ), are not covered: they rest on Tag 0EIE, which this library does not carry”.

Each component of the canonical map (ℱₙ) ⟶ (ℱ'ₙ) is the depth-one quotient of its source: ℱ'ₙ is coherent, the map is surjective and an isomorphism on stalks outside T, and ℱ'ₙ has depth at least one at every point of T.

theorem isDepthOneQuotient_toImprovedSystem_app (n : ℕᵒᵖ) :
    IsDepthOneQuotient T ((toImprovedSystem T hT F).app n)

Stacks.Algebraization.exists_improving_map_of_coherentAdicSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/ImprovingFormalModules.lean, line 133. The attribute's comment: “the canonical map out of an object of Coh(X, ℐ) and its property (1)”.

A coherent adic system along an ideal sheaf admits a map to an inverse system of coherent modules each of whose terms is the quotient of the corresponding term by its sections supported on T, hence has depth at least one along T.

theorem exists_improving_map_of_coherentAdicSystem {I : X.IdealSheafData}
    (F : Stacks.Coherent.CoherentAdicSystems I) :
    ∃ (G : ℕᵒᵖ ⥤ X.Modules) (τ : F.obj ⟶ G), ∀ n : ℕᵒᵖ, IsDepthOneQuotient T (τ.app n)

Stacks.Algebraization.exists_proIso_coherentAdicSystem_toImprovedSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/ImprovingFormalModulesTheorem.lean, line 69. The attribute's comment: “the canonical map (ℱₙ) → (ℱ'ₙ) and its properties (1), (2) and (3); stated for every Noetherian scheme, without the dualizing complex of the source”.

Stacks Project, Tag 0EJE. Let X be a Noetherian scheme, ℐ a quasi-coherent sheaf of ideals with closed subscheme Y, (ℱ_n) an object of Coh(X, ℐ) and T ⊆ Y stable under specialization. Assume that for y ∈ T and every nonmaximal prime 𝔭 of 𝒪_{X,y}^∧ with V(𝔭) ∩ V(ℐ𝒪_{X,y}^∧) = {𝔪_y^∧} the module (ℱ_y^∧)_𝔭 has positive depth. Then the canonical map (ℱ_n) → (ℱ'_n) onto the quotients by the sections supported in T (Stacks.Algebraization.toImprovedSystem, each component the depth-one quotient of Stacks, Tag 0DX3: ℱ'_n coherent, the map surjective and an isomorphism on stalks outside T) has the following properties:

1. every ℱ'_n has depth at least one at every point of T;
2. (ℱ'_n) is isomorphic as a pro-system to an object (𝒢_n) of Coh(X, ℐ): there is a pro-isomorphism P whose forward maps are the components of a morphism ψ : (𝒢_n) → (ℱ'_n);
3. the induced morphism φ : (ℱ_n) → (𝒢_n) of Coh(X, ℐ), the one with φ ≫ ψ the canonical map, is an epimorphism of Coh(X, ℐ) whose kernel in Coh(X, ℐ) is annihilated by a power of ℐ.

The source also assumes that X locally has a dualizing complex; the statement holds without it.

theorem exists_proIso_coherentAdicSystem_toImprovedSystem (hTY : T ⊆ I.support)
    (h6 : ∀ y ∈ T, ∀ p : PrimeSpectrum (completedLocalRing I y),
      p.asIdeal ≠ completedMaximalIdeal I y →
      adicClosedFibreThrough I y p = {completedMaximalIdeal I y} →
      0 < completedStalkDepth I F y p) :
    (∀ n : ℕᵒᵖ, IsDepthOneQuotient T ((toImprovedSystem T hT F.obj).app n)) ∧
    (∀ (n : ℕ) (y : X), y ∈ T →
      letI : Module (X.presheaf.stalk y) (TopCat.Presheaf.stalk (C := Ab.{u})
          ((improvedSystem T hT F.obj).obj (op n)).val.presheaf y) :=
        PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
          (R := X.presheaf) ((improvedSystem T hT F.obj).obj (op n)).val y
      (1 : ℕ∞) ≤ Module.depth (X.presheaf.stalk y) (IsLocalRing.maximalIdeal (X.presheaf.stalk y))
        (TopCat.Presheaf.stalk (C := Ab.{u}) ((improvedSystem T hT F.obj).obj (op n)).val.presheaf
          y)) ∧
    ∃ (G : Stacks.Coherent.CoherentAdicSystems I) (φ : F ⟶ G)
      (ψ : G.obj ⟶ improvedSystem T hT F.obj)
      (P : InverseSequence.ProIso G.obj (improvedSystem T hT F.obj)),
      φ.hom ≫ ψ = toImprovedSystem T hT F.obj ∧
      (∀ m, P.φ m = InverseSequence.tr G.obj (P.αle m) ≫ ψ.app (op m)) ∧
      Epi φ ∧
      ∃ c : ℕ, ∀ n : ℕ, idealPowerMultiple I c ((kernel φ).obj.obj (op n)) = ⊥

Tag 0EJF, a lemma

Tag 0EJF in the Stacks Project.

Stacks.Algebraization.depth_stalk_depthTwoImprovedSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/ImprovingFormalModulesDepthTwo.lean, line 254. The attribute's comment: “conclusions (1) and (2), for T' closed and with the termwise depth-two extensions as data; conclusions (3) and (4) rest on the essential-constancy assertion of Tag 0EIE, which this library carries only as a hypothesis”.

Stacks Project, Tag 0EJF, conclusions (1) and (2). Every term of the depth-two improved system has depth at least one at each point of T and depth at least two at each point of T'.

public theorem depth_stalk_depthTwoImprovedSystem (S : DepthTwoImprovement T T' hT F)
    (n : ℕᵒᵖ) (x : X) :
    letI : Module (X.presheaf.stalk x)
        (TopCat.Presheaf.stalk (C := Ab.{u}) (S.term n).val.presheaf x) :=
      PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
        (R := X.presheaf) (S.term n).val x
    (x ∈ T → (1 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
        (IsLocalRing.maximalIdeal (X.presheaf.stalk x))
        (TopCat.Presheaf.stalk (C := Ab.{u}) (S.term n).val.presheaf x)) ∧
      (x ∈ T' → (2 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
        (IsLocalRing.maximalIdeal (X.presheaf.stalk x))
        (TopCat.Presheaf.stalk (C := Ab.{u}) (S.term n).val.presheaf x))

Stacks.Algebraization.exists_proIso_coherentAdicSystem_canonicalImprovedSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/ImprovingFormalModulesDepthTwoCarrier.lean, line 148.

Stacks Project, Tag 0EJF. Let X be a Noetherian scheme which locally has a dualizing complex, ℐ a quasi-coherent ideal sheaf with support Y, (ℱₙ) an object of Coh(X, ℐ), T' ⊆ T ⊆ Y subsets stable under specialization and d ≥ 0 an integer, such that * (a) every point has an affine neighbourhood U with cd(Γ(X, U), ℐ(U)) ≤ d, * (b) for y ∈ T and a nonmaximal prime 𝔭 of 𝒪_{X,y}^∧ with V(𝔭) ∩ V(ℐ_y^∧) = {𝔪_y^∧}, depth((ℱ_y^∧)_𝔭) > 0, * (c) for y ∈ T' and a prime 𝔭 ∉ V(ℐ_y^∧) of 𝒪_{X,y}^∧ with V(𝔭) ∩ V(ℐ_y^∧) ≠ {𝔪_y^∧}, depth((ℱ_y^∧)_𝔭) ≥ 1 or depth((ℱ_y^∧)_𝔭) + dim(𝒪_{X,y}^∧/𝔭) > 1 + d, * (d) for y ∈ T' and a nonmaximal prime 𝔭 of 𝒪_{X,y}^∧ with V(𝔭) ∩ V(ℐ_y^∧) = {𝔪_y^∧}, depth((ℱ_y^∧)_𝔭) > 1, * (e) if y ⤳ y' is an immediate specialization of points of Y with y' ∈ T', then y ∈ T.

Then the canonical map (ℱₙ) ⟶ (ℱ''ₙ) (each component the improvement of ℱₙ along T' ⊆ T of [Stacks, Tag 0EI4]) satisfies 1. depth(ℱ''_{n,y}) ≥ 1 for y ∈ T, 2. depth(ℱ''_{n,y'}) ≥ 2 for y' ∈ T', 3. (ℱ''ₙ) is pro-isomorphic to an object (ℋₙ) of Coh(X, ℐ), 4. the induced morphism σ : (ℱₙ) ⟶ (ℋₙ) of Coh(X, ℐ) has kernel and cokernel annihilated by a power of ℐ (both in Coh(X, ℐ) and levelwise).

theorem exists_proIso_coherentAdicSystem_canonicalImprovedSystem {X : Scheme.{u}}
    [IsNoetherian X] {I : X.IdealSheafData} (hdual : HasDualizingComplexOnAffineCover X)
    (F : Stacks.Coherent.CoherentAdicSystems I) {T T' : Set X}
    (hT : StableUnderSpecialization T) (hT' : StableUnderSpecialization T')
    (hTY : T ⊆ I.support) (hTT' : T' ⊆ T) (d : ℕ)
    (ha : ∀ x : X, ∃ U : X.affineOpens, x ∈ U.1 ∧
      letI : IsNoetherianRing Γ(X, U.1) := IsLocallyNoetherian.component_noetherian U
      Stacks.LocalCohomology.cohomologicalDimension Γ(X, U.1) (I.ideal U)
        (Ideal.fg_of_isNoetherianRing _) ≤ (d : ℤ))
    (hb : ∀ y ∈ T, ∀ p : PrimeSpectrum (completedLocalRing I y),
      p.asIdeal ≠ completedMaximalIdeal I y →
      adicClosedFibreThrough I y p = {completedMaximalIdeal I y} →
      0 < completedStalkDepth I F y p)
    (hc : ∀ y ∈ T', ∀ p : PrimeSpectrum (completedLocalRing I y),
      ¬ completedLocalIdeal I y ≤ p.asIdeal →
      adicClosedFibreThrough I y p ≠ {completedMaximalIdeal I y} →
      1 ≤ completedStalkDepth I F y p ∨
        enatToEInt (completedStalkDepth I F y p) +
            krullDimToEInt (ringKrullDim (completedLocalRing I y ⧸ p.asIdeal)) >
          ((1 + d : ℤ) : EInt))
    (hd : ∀ y ∈ T', ∀ p : PrimeSpectrum (completedLocalRing I y),
      p.asIdeal ≠ completedMaximalIdeal I y →
      adicClosedFibreThrough I y p = {completedMaximalIdeal I y} →
      1 < completedStalkDepth I F y p)
    (himm : ∀ x x' : X, x ∈ I.support → IsImmediateSpecialization x x' → x' ∈ T' → x ∈ T) :
    (∀ (n : ℕᵒᵖ) (x : X),
      letI : Module (X.presheaf.stalk x)
          (TopCat.Presheaf.stalk (C := Ab.{u})
            ((canonicalImprovedSystem hdual F hT hT' hTY himm).obj n).val.presheaf x) :=
        PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
          (R := X.presheaf) ((canonicalImprovedSystem hdual F hT hT' hTY himm).obj n).val x
      (x ∈ T → (1 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
          (IsLocalRing.maximalIdeal (X.presheaf.stalk x))
          (TopCat.Presheaf.stalk (C := Ab.{u})
            ((canonicalImprovedSystem hdual F hT hT' hTY himm).obj n).val.presheaf x)) ∧
        (x ∈ T' → (2 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
          (IsLocalRing.maximalIdeal (X.presheaf.stalk x))
          (TopCat.Presheaf.stalk (C := Ab.{u})
            ((canonicalImprovedSystem hdual F hT hT' hTY himm).obj n).val.presheaf x))) ∧
    (∀ n : ℕᵒᵖ, IsNestedImprovement T T'
      ((toCanonicalImprovedSystem hdual F hT hT' hTY himm).app n)) ∧
    ∃ (H : Stacks.Coherent.CoherentAdicSystems I)
      (e : InverseSequence.ProIso (canonicalImprovedSystem hdual F hT hT' hTY himm) H.obj)
      (σ : F ⟶ H),
      (∀ n : ℕ, (toCanonicalImprovedSystem hdual F hT hT' hTY himm).app (op (e.α n)) ≫ e.φ n =
        F.obj.map (homOfLE (e.αle n)).op ≫ σ.hom.app (op n)) ∧
      (∃ c : ℕ, ∀ n : ℕ, idealPowerMultiple I c ((kernel σ).obj.obj (op n)) = ⊥) ∧
      (∃ c : ℕ, ∀ n : ℕ, idealPowerMultiple I c ((cokernel σ).obj.obj (op n)) = ⊥) ∧
      IsKernelCokernelAnnihilatedByPower I σ.hom

Tag 0EJG, a lemma

Tag 0EJG in the Stacks Project.

Stacks.Algebraization.exists_proIso_coherentAdicSystem_depthThreeImprovedSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/ImprovingFormalModulesDepthThreeCarrier.lean, line 66.

[Stacks, Tag 0EJG]. Let A have a dualizing complex, let d ≥ cd(A, I) and let (ℱₙ) in Coh(U, I𝒪_U) satisfy the (2, 2 + d)-inequalities. Then there is a map (ℱₙ) ⟶ (ℱ''ₙ) of inverse systems of coherent 𝒪_U-modules with (1) depth(ℱ''_{n,y}) + δ^Y_Z(y) ≥ 3 on U ∩ Y, (2) (ℱ''ₙ) pro-isomorphic to an object (ℋₙ) of Coh(U, I𝒪_U), compatibly with the maps from (ℱₙ), (3) the induced morphism (ℱₙ) ⟶ (ℋₙ) with kernel and cokernel annihilated by a power of I, both in Coh(U, I𝒪_U) and termwise, and (4) Hᵖ(U, ℱ''ₙ) a finite A-module for p ≤ 1 and all n.

public theorem exists_proIso_coherentAdicSystem_depthThreeImprovedSystem
    (S : AlgebraizationSituation.{u})
    (hdual : ∃ K : DerivedCategory (ModuleCat.{u} S.A), Dualizing.IsDualizingComplex K)
    (d : ℤ) (hd : cohomologicalDimension S.A S.I (Ideal.fg_of_isNoetherianRing S.I) ≤ d)
    (F : Stacks.Coherent.CoherentAdicSystems (idealOnOpen S))
    (h : SatisfiesDepthInequalities S F 2 (2 + d)) :
    ∃ (F'' : ℕᵒᵖ ⥤ S.U.toScheme.Modules) (τ : F.obj ⟶ F''),
      (∀ n : ℕᵒᵖ, (F''.obj n).IsCoherent) ∧
      (∀ (n : ℕᵒᵖ) (y : S.U.toScheme) (z : S.Y), S.U.ι.base y = S.Yι.base z →
        (3 : ℕ∞) ≤ Module.depth (S.U.toScheme.presheaf.stalk y)
            (maximalIdeal (S.U.toScheme.presheaf.stalk y)) ((F''.obj n).presheaf.stalk y) +
          S.distanceToZ z) ∧
      (∃ (H : Stacks.Coherent.CoherentAdicSystems (idealOnOpen S))
        (e : InverseSequence.ProIso F'' H.obj) (σ : F ⟶ H),
        (∀ n : ℕ, τ.app (op (e.α n)) ≫ e.φ n =
          F.obj.map (homOfLE (e.αle n)).op ≫ σ.hom.app (op n)) ∧
        (∃ c : ℕ, ∀ n : ℕ,
          idealPowerMultiple (idealOnOpen S) c ((kernel σ).obj.obj (op n)) = ⊥) ∧
        (∃ c : ℕ, ∀ n : ℕ,
          idealPowerMultiple (idealOnOpen S) c ((cokernel σ).obj.obj (op n)) = ⊥) ∧
        IsKernelCokernelAnnihilatedByPower (idealOnOpen S) σ.hom) ∧
      (∀ (n : ℕᵒᵖ) (p : ℕ), p ≤ 1 →
        Module.Finite S.A ((complementSheafCohomology S.A S.a p).obj (F''.obj n)))

Sources

• Section 52.21, Tag 0EJD
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Algebraization.finite_completedStalk · Stacks.Algebraization.isDepthOneQuotient_toImprovedSystem_app · Stacks.Algebraization.exists_improving_map_of_coherentAdicSystem · Stacks.Algebraization.exists_proIso_coherentAdicSystem_toImprovedSystem · Stacks.Algebraization.depth_stalk_depthTwoImprovedSystem · Stacks.Algebraization.exists_proIso_coherentAdicSystem_canonicalImprovedSystem · Stacks.Algebraization.exists_proIso_coherentAdicSystem_depthThreeImprovedSystem

Section52.22 Algebraization of coherent formal modules, V#

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

Tag 0EJI, a lemma

Tag 0EJI in the Stacks Project.

Stacks.Algebraization.canonicallyExtends_of_cd_one_of_proIso_depthThree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/CanonicalExtensionCdOneDepthThree.lean, line 102.

Stacks Project, Tag 0EJI. In Situation 0EHC let (ℱₙ) be an object of Coh(U, I𝒪_U). Assume (1) A has a dualizing complex and cd(A, I) = 1, and (2) (ℱₙ) is pro-isomorphic to an inverse system (ℱ''ₙ) of coherent 𝒪_U-modules with depth(ℱ''_{n,y}) + δ^Y_Z(y) ≥ 3 for all y ∈ U ∩ Y. Then (ℱₙ) extends canonically to X.

A point of U ∩ Y is a point y of U together with a point z of Y with the same image in X; the depth is that of the stalk over the local ring of U at y, and δ^Y_Z is evaluated at z.

theorem canonicallyExtends_of_cd_one_of_proIso_depthThree
    (hdual : ∃ K : DerivedCategory (ModuleCat.{u} S.A), Dualizing.IsDualizingComplex K)
    (hcd : Stacks.LocalCohomology.cohomologicalDimension S.A S.I
      (IsNoetherian.noetherian S.I) = 1)
    (G : ℕᵒᵖ ⥤ S.U.toScheme.Modules) [∀ n : ℕᵒᵖ, (G.obj n).IsCoherent]
    (e : InverseSequence.ProIso F.obj G)
    (hdepth : ∀ n : ℕ, ∀ (y : S.U.toScheme) (z : S.Y), S.U.ι.base y = S.Yι.base z →
      3 ≤ depthOfStalkOnOpen S (G.obj (op n)) y + S.distanceToZ z) :
    CanonicallyExtends S F

Tag 0EJJ, a proposition

Tag 0EJJ in the Stacks Project.

Stacks.Algebraization.extendsToX_of_cd_one_of_satisfiesDepthInequalities, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/AlgebraizationCdOneTheorem.lean, line 80. The attribute's comment: “(ℱₙ) extends to X”.

Stacks Project, Tag 0EJJ (algebraization in cohomological dimension one). In Situation 0EHC let (ℱₙ) be an object of Coh(U, I𝒪_U). Assume (1) A has a dualizing complex and cd(A, I) = 1, and (2) (ℱₙ) satisfies the (2, 3)-inequalities. Then (ℱₙ) extends to X.

public theorem extendsToX_of_cd_one_of_satisfiesDepthInequalities
    (F : Stacks.Coherent.CoherentAdicSystems (idealOnOpen S))
    (hdual : ∃ K : DerivedCategory (ModuleCat.{u} S.A), Dualizing.IsDualizingComplex K)
    (hcd : Stacks.LocalCohomology.cohomologicalDimension S.A S.I
      (IsNoetherian.noetherian S.I) = 1)
    (hineq : SatisfiesDepthInequalities S F 2 3) :
    ExtendsToX S (toKerSystem S F)

Stacks.Algebraization.isCompletion_of_cd_one_of_satisfiesDepthInequalities, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/AlgebraizationCdOneTheorem.lean, line 100. The attribute's comment: “in particular, for I-adically complete A, (ℱₙ) is the completion of a coherent 𝒪_U-module”.

Stacks Project, Tag 0EJJ, the final clause. In the situation of Tag 0EJJ, if moreover A is I-adically complete, then (ℱₙ) is the completion of a coherent 𝒪_U-module.

public theorem isCompletion_of_cd_one_of_satisfiesDepthInequalities [IsAdicComplete S.I S.A]
    (F : Stacks.Coherent.CoherentAdicSystems (idealOnOpen S))
    (hdual : ∃ K : DerivedCategory (ModuleCat.{u} S.A), Dualizing.IsDualizingComplex K)
    (hcd : Stacks.LocalCohomology.cohomologicalDimension S.A S.I
      (IsNoetherian.noetherian S.I) = 1)
    (hineq : SatisfiesDepthInequalities S F 2 3) :
    (completionFunctor S.U.toScheme (S.Yι.ker.comap S.U.ι)).essImage (toKerSystem S F)

Tag 0EJK, a lemma

Tag 0EJK in the Stacks Project.

Stacks.Algebraization.extendsToX_of_blowUp_fiber_dim_lt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/AlgebraizationBlowupFibres.lean, line 410. The attribute's comment: “the whole statement: under (1) a dualizing complex, (2) fibres of the blowup of I of dimension ≤ d - 1, (3) the (d + 1, d + 2)-inequalities or the bound depth + dim + δ > d + 2, the object (ℱₙ) of Coh(U, I𝒪_U) extends to X”.

Stacks Project, Tag 0EJK. In Situation [Stacks, Tag 0EHC] let (ℱₙ) be an object of Coh(U, I𝒪_U). Assume

1. A has a dualizing complex,
2. all fibres of the blowing up b : X' → X of I have dimension ≤ d - 1, and
3. one of the following is true: (a) (ℱₙ) satisfies the (d + 1, d + 2)-inequalities ([Stacks, Tag 0EJ3]), or (b) for y ∈ U ∩ Y and a prime 𝔭 ⊆ 𝒪^∧_{X,y} with 𝔭 ∉ V(I𝒪^∧_{X,y}) we have depth((ℱ^∧_y)_𝔭) + dim(𝒪^∧_{X,y}/𝔭) + δ^Y_Z(y) > d + 2.

Then (ℱₙ) extends to X.

Here d is an integer and the fibre condition dim ≤ d - 1 is written dim < d for the natural number d.toNat, which is the same condition (for d ≤ 0 both say every fibre is empty). The dualizing complex lives in the derived category HasDerivedCategory.standard, as in [Stacks, Tag 0EJJ].

theorem extendsToX_of_blowUp_fiber_dim_lt (F : Stacks.Coherent.CoherentAdicSystems (idealOnOpen S))
    (d : ℤ)
    (hdual : ∃ K : @DerivedCategory (ModuleCat.{u} S.A) _ _
      (HasDerivedCategory.standard (ModuleCat.{u} S.A)),
      @Dualizing.IsDualizingComplex S.A _ _ (HasDerivedCategory.standard (ModuleCat.{u} S.A)) K)
    (hfib : ∀ y : Spec (CommRingCat.of S.A), topologicalKrullDim ((AlgebraicGeometry.blowUpToBase
      (Stacks.LocalCohomology.specIdealSheaf S.A S.I)).fiber y) < ((d.toNat : ℕ) : WithBot ℕ∞))
    (h3 : SatisfiesDepthInequalities S F (d + 1) (d + 2) ∨
      ∀ (y : S.U.toScheme) (z : S.Y), S.U.ι.base y = S.Yι.base z →
        ∀ p : PrimeSpectrum (completedLocalRing (idealOnOpen S) y),
          ¬ completedLocalIdeal (idealOnOpen S) y ≤ p.asIdeal →
          depthAddDimAddDistance S F y z p > ((d + 2 : ℤ) : EInt)) :
    ExtendsToX S (toKerSystem S F)

Tag 0EJN, a proposition

Tag 0EJN in the Stacks Project.

Stacks.Algebraization.algebraization_of_zeroLocus_eq_range_of_depthBound, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/AlgebraizationFewGenerators.lean, line 131. The attribute's comment: “the whole statement: (F_n) extends to X, and over an I-adically complete A it is the completion of a coherent O_U-module”.

Stacks Project, Tag 0EJN (Algebraization for ideals with few generators). In Situation 0EHC let (ℱₙ) be an object of Coh(U, I𝒪_U). Assume (1) A has a dualizing complex, (2) V(I) = V(f₁, …, f_d) for some d ≥ 1, and (3) (ℱₙ) satisfies the (d + 1, d + 2)-inequalities or depth((ℱ_y^∧)_𝔭) + dim(𝒪_{X,y}^∧/𝔭) + δ^Y_Z(y) > d + 2 at every y ∈ U ∩ Y and every prime 𝔭 ∉ V(I𝒪_{X,y}^∧). Then (ℱₙ) extends to X, and if A is I-adically complete then (ℱₙ) is the completion of a coherent 𝒪_U-module.

public theorem algebraization_of_zeroLocus_eq_range_of_depthBound
    (S : AlgebraizationSituation.{u}) [HasDerivedCategory.{w} (ModuleCat.{u} S.A)]
    (F : Stacks.Coherent.CoherentAdicSystems (idealOnOpen S))
    (hdual : ∃ K : DerivedCategory (ModuleCat.{u} S.A), Dualizing.IsDualizingComplex K)
    (d : ℕ) (hd : 1 ≤ d) (f : Fin d → S.A)
    (hV : PrimeSpectrum.zeroLocus (S.I : Set S.A) = PrimeSpectrum.zeroLocus (Set.range f))
    (h3 : SatisfiesDepthInequalities S F (d + 1) (d + 2) ∨
      ∀ (y : S.U.toScheme) (z : S.Y), S.U.ι.base y = S.Yι.base z →
        ∀ p : PrimeSpectrum (completedLocalRing (idealOnOpen S) y),
          ¬ completedLocalIdeal (idealOnOpen S) y ≤ p.asIdeal →
          depthAddDimAddDistance S F y z p > ((d + 2 : ℤ) : EInt)) :
    ExtendsToX S (toKerSystem S F) ∧
      (IsAdicComplete S.I S.A →
        (completionFunctor S.U.toScheme (S.Yι.ker.comap S.U.ι)).essImage (toKerSystem S F))

Tag 0EJP, a lemma

Tag 0EJP in the Stacks Project.

Stacks.Algebraization.extendsToX_and_essImage_of_isCohenMacaulay_of_span_eq_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/AlgebraizationFewGeneratorsCohenMacaulay.lean, line 92. The attribute's comment: “the whole statement: under hypotheses (1)-(6) the system extends to X, and over an I-adically complete A it is the completion of a coherent O_U-module; the example in (6) is free_localizedModule_completedStalk_of_isFiniteLocallyFreeAdic”.

Stacks Project, Tag 0EJP. In Situation 0EHC let (ℱₙ) be an object of Coh(U, I𝒪_U). Assume

1. A is a local ring which has a dualizing complex,
2. all irreducible components of X have the same dimension,
3. the scheme X \ Y is Cohen–Macaulay,
4. I is generated by d elements,
5. dim(X) - dim(Z) > d + 2, and
6. for y ∈ U ∩ Y the module ℱ_y^∧ is finite locally free outside V(I𝒪_{X,y}^∧) (for example if ℱₙ is a finite locally free 𝒪_U/Iⁿ𝒪_U-module, see free_localizedModule_completedStalk_of_isFiniteLocallyFreeAdic).

Then (ℱₙ) extends to X. In particular if A is I-adically complete, then (ℱₙ) is the completion of a coherent 𝒪_U-module.

public theorem extendsToX_and_essImage_of_isCohenMacaulay_of_span_eq_range
    (S : AlgebraizationSituation.{u}) [HasDerivedCategory.{w} (ModuleCat.{u} S.A)]
    [IsLocalRing S.A] (F : Stacks.Coherent.CoherentAdicSystems (idealOnOpen S))
    (hdual : ∃ K : DerivedCategory (ModuleCat.{u} S.A), Dualizing.IsDualizingComplex K)
    (hequi : Equidimensional (PrimeSpectrum S.A))
    (hCM : ∀ q : PrimeSpectrum S.A, ¬ S.I ≤ q.asIdeal →
      IsCohenMacaulayLocalRing (Localization.AtPrime q.asIdeal))
    (d : ℕ) (f : Fin d → S.A) (hI : S.I = Ideal.span (Set.range f))
    (hdim : ringKrullDim (S.A ⧸ S.a) + ((d + 2 : ℕ) : WithBot ℕ∞) < ringKrullDim S.A)
    (hfree : ∀ (y : S.U.toScheme) (z : S.Y), S.U.ι.base y = S.Yι.base z →
      ∀ p : PrimeSpectrum (completedLocalRing (idealOnOpen S) y),
        ¬ completedLocalIdeal (idealOnOpen S) y ≤ p.asIdeal →
        Module.Free (Localization.AtPrime p.asIdeal)
          (LocalizedModule p.asIdeal.primeCompl (completedStalk (idealOnOpen S) F y))) :
    ExtendsToX S (toKerSystem S F) ∧
      (IsAdicComplete S.I S.A →
        (completionFunctor S.U.toScheme (S.Yι.ker.comap S.U.ι)).essImage (toKerSystem S F))

Sources

• Section 52.22, Tag 0EJH
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Algebraization.canonicallyExtends_of_cd_one_of_proIso_depthThree · Stacks.Algebraization.extendsToX_of_cd_one_of_satisfiesDepthInequalities · Stacks.Algebraization.isCompletion_of_cd_one_of_satisfiesDepthInequalities · Stacks.Algebraization.extendsToX_of_blowUp_fiber_dim_lt · Stacks.Algebraization.algebraization_of_zeroLocus_eq_range_of_depthBound · Stacks.Algebraization.extendsToX_and_essImage_of_isCohenMacaulay_of_span_eq_range

Section52.23 Algebraization of coherent formal modules, VI#

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

Tag 0EJS, a proposition

Tag 0EJS in the Stacks Project.

Stacks.Algebraization.finite_globalSections_of_finite_idealPowerSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/RegularSequence.lean, line 185. The attribute's comment: “the induction giving finiteness of every H⁰(U, Fₙ), with the direct-sum decomposition of Iⁿ F₍ₙ₊₁₎ replaced by the hypothesis that its sections are finite”.

Stacks Project, Tag 0EJS (the induction of the proof). If H⁰(U, F_1) is a finite A-module and every H⁰(U, I^(n+1) F_(n+1)) is a finite A-module, then H⁰(U, F_n) is a finite A-module for every n.

This is the step "using the assumption of finiteness of H⁰(U, F_1) and induction, we first conclude that M_n = H⁰(U, F_n) is a finite A-module for all n" of the source. The source gets finiteness of H⁰(U, I^(n+1) F_(n+1)) from the stalkwise direct-sum decomposition of I^(n+1) F_(n+1) into copies of F_1, which is not available in this library; here it is a hypothesis.

theorem finite_globalSections_of_finite_idealPowerSections
    (h0 : Module.Finite S.A ((globalSectionsSystem S F).obj (op 0)))
    (hker : ∀ n, Module.Finite S.A (idealPowerSections S F n)) :
    ∀ n, Module.Finite S.A ((globalSectionsSystem S F).obj (op n))

Stacks.Algebraization.canonicallyExtends_of_finite_globalSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/RegularSequence.lean, line 221. The attribute's comment: “the reduction to Tag 0EHH: condition (c) from finiteness of every H⁰(U, Fₙ), with conditions (a) and (b) as hypotheses”.

Stacks Project, Tag 0EJS (condition (c) of Tag 0EHH). Finiteness of every H⁰(U, F_n) implies the finite-image condition (c) of the Mittag-Leffler criterion Stacks 0EHH, so together with the Mittag-Leffler condition (a) and the topology condition (b) it gives canonical extension.

The source derives (a) and (b) from Cohomology 0GYK and 0GYM applied to the graded module ⨁_n H^p(U, IⁿF_(n+1)); here they are hypotheses.

theorem canonicallyExtends_of_finite_globalSections
    (hML : IsMittagLefflerCategorical (globalSectionsSystem S F))
    (htop : (⨅ n : ℕ, TopologicalSpace.induced
      (fun x : limitGlobalSections S F =>
        (limit.π (globalSectionsSystem S F) (op n)).hom x) ⊥) =
        S.I.adicModuleTopology (limitGlobalSections S F))
    (hfin : ∀ n, Module.Finite S.A ((globalSectionsSystem S F).obj (op n))) :
    CanonicallyExtends S F

Stacks.Algebraization.canonicallyExtends_of_finite_idealPowerSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/RegularSequence.lean, line 240. The attribute's comment: “the finiteness half: conditions (a), (b) of Tag 0EHH and finiteness of the sections of Iⁿ F₍ₙ₊₁₎ are hypotheses instead of consequences of the regular sequence”.

Stacks Project, Tag 0EJS (the finiteness half). A coherent adic system on the open complement extends canonically to X as soon as its system of global sections has Mittag-Leffler, the limit topology on the module of compatible sections is the I-adic topology, H⁰(U, F_1) is a finite A-module, and every H⁰(U, I^(n+1) F_(n+1)) is a finite A-module.

theorem canonicallyExtends_of_finite_idealPowerSections
    (hML : IsMittagLefflerCategorical (globalSectionsSystem S F))
    (htop : (⨅ n : ℕ, TopologicalSpace.induced
      (fun x : limitGlobalSections S F =>
        (limit.π (globalSectionsSystem S F) (op n)).hom x) ⊥) =
        S.I.adicModuleTopology (limitGlobalSections S F))
    (h0 : Module.Finite S.A ((globalSectionsSystem S F).obj (op 0)))
    (hker : ∀ n, Module.Finite S.A (idealPowerSections S F n)) :
    CanonicallyExtends S F

Stacks.Algebraization.HasRegularSequenceOnCompletedStalks, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/RegularSequence.lean, line 273. The attribute's comment: “hypothesis (1), as a predicate; not used by any result in this file”.

Stacks Project, Tag 0EJS, hypothesis (1). There are f₁, …, f_d ∈ I such that at every point y of U ∩ Y the ideal I 𝒪_{X,y} is generated by the germs of f₁, …, f_d and those germs form an F_y^∧-regular sequence.

The locus U ∩ Y is the support of the ideal sheaf I 𝒪_U, and F_y^∧ is Stacks.Algebraization.completedStalk. The sequence is taken as a sequence of elements of the local ring 𝒪_{X,y} acting on F_y^∧, which is how the source's f_i ∈ I ⊆ A act.

def HasRegularSequenceOnCompletedStalks : Prop

Stacks.Algebraization.HasFiniteLowDegreeCohomology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/RegularSequence.lean, line 287. The attribute's comment: “hypothesis (2), as a predicate; not used by any result in this file”.

Stacks Project, Tag 0EJS, hypothesis (2). H⁰(U, F_1) and H¹(U, F_1) are finite A-modules.

Degree zero is the global-sections module of the system, and degree one is the first right derived functor of sections over the base, Stacks.LocalCohomology.cohomologyOverBase.

def HasFiniteLowDegreeCohomology : Prop

Stacks.Algebraization.canonicallyExtends_of_regularSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/RegularSequenceCanonicalExtension.lean, line 407. The attribute's comment: “the system extends canonically to X”.

Stacks Project, Tag 0EJS. In Situation 0EHC let (F_n) be an object of Coh(U, I 𝒪_U). Assume that

1. there exist f₁, …, f_d ∈ I such that for y ∈ U ∩ Y the ideal I 𝒪_{X,y} is generated by f₁, …, f_d and f₁, …, f_d form an F_y^∧-regular sequence (Stacks.Algebraization.HasRegularSequenceOnCompletedStalks),
2. H⁰(U, F_1) and H¹(U, F_1) are finite A-modules (Stacks.Algebraization.HasFiniteLowDegreeCohomology).

Then (F_n) extends canonically to X.

The proof is the source's: the decomposition Stacks.Algebraization.exists_isIso_idealPowerDesc_of_regularSequence of Iⁿ F_(n+1) into copies of F_1 indexed by the monomials in the fᵢ, fed to Stacks.Algebraization.canonicallyExtends_of_idealPowerDesc, which verifies conditions (a), (b), (c) of Stacks 0EHH.

theorem canonicallyExtends_of_regularSequence (hreg : HasRegularSequenceOnCompletedStalks S F)
    (h2 : HasFiniteLowDegreeCohomology S F) : CanonicallyExtends S F

Stacks.Algebraization.essImage_completionFunctor_of_regularSequence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/RegularSequenceCanonicalExtension.lean, line 418. The attribute's comment: “in particular, if A is complete, the system is the completion of a coherent 𝒪_U-module”.

Stacks Project, Tag 0EJS, the second sentence. Under the hypotheses of Stacks 0EJS, if A is moreover I-adically complete, then (F_n) is the completion of a coherent 𝒪_U-module.

theorem essImage_completionFunctor_of_regularSequence [IsAdicComplete S.I S.A]
    (hreg : HasRegularSequenceOnCompletedStalks S F) (h2 : HasFiniteLowDegreeCohomology S F) :
    (completionFunctor S.U.toScheme (idealOnOpen S)).essImage F

Tag 0EJT, a remark

Tag 0EJT in the Stacks Project.

Stacks.Algebraization.hasFiniteLowDegreeCohomology_iff_hasDepthDimensionAt_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/FinitenessDepthCriterion.lean, line 192. The attribute's comment: “the equivalence; only the formal-fibre step and an H^p(U, F₁) bridge are assumed”.

Stacks Project, Tag 0EJT (the equivalence). Assume A has a dualizing complex. Then hypothesis (2) of Stacks 0EJS, that H⁰(U, F_1) and H¹(U, F_1) are finite A-modules, holds if and only if depth(F_{1,y}) + dim(𝒪_{closure{y}, z}) > 2 for every y ∈ U ∩ Y and every z ∈ Z ∩ closure{y}.

The right-hand side is Stacks.Algebraization.HasDepthDimensionAt at 2 for a finite A-module M whose associated sheaf restricts to F_1 on U. The equivalence is the criterion of Stacks 0BJY at n = 2, which is proved here as Stacks.Algebraization.affineDepthDimensionCriterion; the dualizing complex discharges its catenarity assumption by Stacks 0A80 and enters the proof only through that and through hformalOfDual. The two comparison hypotheses are a bridge between two spellings of the same A-module H^p(U, F_1) and assume nothing about the situation, and the passage from complementCohomologyBase to coherence of the higher direct images is clause (3) of Stacks 0BK0 and is proved.

public theorem hasFiniteLowDegreeCohomology_iff_hasDepthDimensionAt_two
    (F : Stacks.Coherent.CoherentAdicSystems (idealOnOpen S))
    (M : ModuleCat.{u} (CommRingCat.of S.A)) (hM : Module.Finite S.A M)
    (hdual : ∃ K : DerivedCategory (ModuleCat.{u} S.A), Dualizing.IsDualizingComplex K)
    (hformalOfDual :
      (∃ K : DerivedCategory (ModuleCat.{u} S.A), Dualizing.IsDualizingComplex K) →
        ∀ q : PrimeSpectrum S.A,
          Stacks.LocalCohomology.FormalFibersHavePropertySk
            (Localization.AtPrime q.asIdeal) 2)
    (hcompare₀ : Module.Finite S.A ((globalSectionsSystem S F).obj (op 0)) ↔
      Module.Finite S.A (complementCohomologyBase (A := CommRingCat.of S.A) S.a M 0))
    (hcompare₁ : Module.Finite S.A
        (Stacks.LocalCohomology.cohomologyOverBase.{u, u} S.A S.U.ι (F.obj.obj (op 0)) 1) ↔
      Module.Finite S.A (complementCohomologyBase (A := CommRingCat.of S.A) S.a M 1)) :
    HasFiniteLowDegreeCohomology S F ↔ HasDepthDimensionAt S M 2

Stacks.Algebraization.hasDepthDimensionAt_two_of_pointwiseBounds, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/FinitenessDepthCriterion.lean, line 321. The attribute's comment: “the trailing sufficient condition, via the two pointwise bounds it yields”.

Stacks Project, Tag 0EJT (the sufficient condition). The depth–dimension inequality at 2 holds when F_1 is finite locally free on 𝒪_{U ∩ Y}, Y is (S₂), and codim(Z', Y') ≥ 3 for every pair of irreducible components Y' of Y and Z' of Z with Z' ⊆ Y'.

The two pointwise bounds that the condition yields are hypotheses, for one reason each. PointwiseSerreTwoBound would follow from (S₂) for Y by way of the depth of a finite locally free module over a local ring being the depth of that ring, and that statement has no public form in this library; the other two steps it needs do, namely moduleDepth_eq_depth and Module.depth_eq_depth_map_algebraMap. PointwiseCodimensionThreeBound would follow from the codimension clause by additivity of codimension along a chain, which is available as catenary_height_add, but in the direction required that needs A to be catenary, and catenarity is not part of the condition stated by the source. What is proved here is that those two bounds, together with the positivity of dim(𝒪_{closure{y},z}) for z strictly above y, give the inequality.

public theorem hasDepthDimensionAt_two_of_pointwiseBounds
    (M : ModuleCat.{u} (CommRingCat.of S.A))
    (N : ModuleCat.{u} (CommRingCat.of (S.A ⧸ S.I)))
    (hcond : HasLocallyFreeCodimensionThreeCondition S N)
    (hserre : PointwiseSerreTwoBound S M N)
    (hcodim : PointwiseCodimensionThreeBound S M N) :
    HasDepthDimensionAt S M 2

Stacks.Algebraization.finite_lowDegreeCohomology_iff_depthDimension_of_isDualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/FinitenessDepthCriterionDualizing.lean, line 572. The attribute's comment: “the equivalence and the sufficient condition”.

Stacks Project, Tag 0EJT. In Situation 0EHC, let (F_n) be a coherent I-adic system on U = Spec A ∖ V(𝔞), as in Stacks 0EJS, and assume A has a dualizing complex.

• H⁰(U, F₁) and H¹(U, F₁) are finite A-modules if and only if depth(F_{1,y}) + dim(𝒪_{closure{y}, z}) > 2 for all y ∈ U ∩ Y and z ∈ Z ∩ closure{y}. The depth is that of the stalk of F₁ at y over 𝒪_{U,y}; the point z is a prime 𝔮 of A containing 𝔞 and the prime 𝔭 of y, and dim(𝒪_{closure{y}, z}) is the height of the image of 𝔮 in A ⧸ 𝔭.
• This holds if F₁ is a finite locally free 𝒪_{U ∩ Y}-module, that is its pullback along the closed immersion U ∩ Y ⟶ U is finite locally free, Y = Spec(A ⧸ I) is (S₂), and codim(Z', Y') ≥ 3 for every pair of irreducible components Y' of Y and Z' of Z with Z' ⊆ Y'. The components of Y and Z are the minimal primes of I and of 𝔞, Z' ⊆ Y' is the inclusion of those primes, and codim(Z', Y') is the height of the image of the prime of Z' in the quotient by the prime of Y'.

theorem finite_lowDegreeCohomology_iff_depthDimension_of_isDualizingComplex
    (F : Stacks.Coherent.CoherentAdicSystems (idealOnOpen S))
    (K : DerivedCategory (ModuleCat.{u} S.A)) (hK : Dualizing.IsDualizingComplex K) :
    (HasFiniteLowDegreeCohomology S F ↔
      ∀ y : S.U.toScheme, S.I ≤ (underlyingPrime S y).asIdeal →
        ∀ q : PrimeSpectrum S.A, S.a ≤ q.asIdeal → (underlyingPrime S y).asIdeal ≤ q.asIdeal →
          (2 : ℕ∞) < Module.depth (S.U.toScheme.presheaf.stalk y)
              (IsLocalRing.maximalIdeal (S.U.toScheme.presheaf.stalk y))
              ((F.obj.obj (op 0)).presheaf.stalk y) +
            (q.asIdeal.map (Ideal.Quotient.mk (underlyingPrime S y).asIdeal)).height) ∧
      (Scheme.Modules.IsFiniteLocallyFree
          ((Scheme.Modules.pullback (intersectionUYι S)).obj (F.obj.obj (op 0))) →
        PropertySkRing (S.A ⧸ S.I) 2 →
        (∀ p ∈ S.I.minimalPrimes, ∀ q ∈ S.a.minimalPrimes, p ≤ q →
          3 ≤ (q.map (Ideal.Quotient.mk p)).height) →
        HasFiniteLowDegreeCohomology S F ∧
          ∀ y : S.U.toScheme, S.I ≤ (underlyingPrime S y).asIdeal →
            ∀ q : PrimeSpectrum S.A, S.a ≤ q.asIdeal → (underlyingPrime S y).asIdeal ≤ q.asIdeal →
              (2 : ℕ∞) < Module.depth (S.U.toScheme.presheaf.stalk y)
                  (IsLocalRing.maximalIdeal (S.U.toScheme.presheaf.stalk y))
                  ((F.obj.obj (op 0)).presheaf.stalk y) +
                (q.asIdeal.map (Ideal.Quotient.mk (underlyingPrime S y).asIdeal)).height)

Tag 0EJU, a proposition

Tag 0EJU in the Stacks Project.

Stacks.Algebraization.canonicallyExtends_of_flatLocalBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/FlatLocalBaseCanonicalExtension.lean, line 493.

Stacks Project, Tag 0EJU. In Situation 0EHC let (F_n) be a coherent I-adic system on U, and let (R, 𝔪) be a Noetherian local ring with a ring map R → A such that I = 𝔪 A and the formal stalks F_y^∧, y ∈ U ∩ Y, are R-flat (both recorded by B), and suppose that H⁰(U, F_1) and H¹(U, F_1) are finite A-modules. Then (F_n) extends canonically to X.

The proof verifies the three conditions of Stacks 0EHH: (a) is Stacks.Algebraization.isMittagLeffler_globalSectionsSystem_of_flatLocalBase, (b) is Stacks.Algebraization.limitTopology_eq_adicModuleTopology_of_flatLocalBase, and (c) comes from the finiteness of every H⁰(U, Iⁿ F_(n+1)), which the direct-sum decomposition Stacks.Algebraization.exists_isoDirectSum_idealPowerSub gives.

theorem canonicallyExtends_of_flatLocalBase (B : FlatLocalBase S F)
    (h3 : HasFiniteLowDegreeCohomology S F) : CanonicallyExtends S F

Stacks.Algebraization.essImage_completionFunctor_of_flatLocalBase, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/FlatLocalBaseCanonicalExtension.lean, line 505. The attribute's comment: “in particular, over an I-adically complete A the system is the completion of a coherent 𝒪_U-module”.

Stacks Project, Tag 0EJU, the concluding sentence. Under the hypotheses of Stacks 0EJU, if A is moreover I-adically complete, then (F_n) is the completion of a coherent 𝒪_U-module.

theorem essImage_completionFunctor_of_flatLocalBase [IsAdicComplete S.I S.A]
    (B : FlatLocalBase S F) (h3 : HasFiniteLowDegreeCohomology S F) :
    (completionFunctor S.U.toScheme (idealOnOpen S)).essImage F

Tag 0EJV, a remark

Tag 0EJV in the Stacks Project.

Stacks.Algebraization.isCompletionOfCoherent_of_flat_of_isCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/ProperLocalBaseAlgebraization.lean, line 82. The attribute's comment: “algebraization: a flat object of Coh(U, 𝔪𝒪_U) with j_F₁ and R¹j_F₁ coherent is the completion of a coherent 𝒪_U-module”.

Stacks 0EJV, algebraization over a complete local base. Let (R, 𝔪) be a complete Noetherian local ring, let p : X ⟶ Spec R be proper, let Z be a closed subset of the special fibre X_1, let U = X ∖ Z with inclusion j = U.ι, and let (F_n) be an object of Coh(U, 𝔪𝒪_U). Assume that F_n is flat over R/𝔪ⁿ for all n, and that j_*F_1 and R¹j_*F_1 are coherent. Then (F_n) is the completion of a coherent 𝒪_U-module.

theorem isCompletionOfCoherent_of_flat_of_isCoherent
    (R : Type u) [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    [IsAdicComplete (IsLocalRing.maximalIdeal R) R]
    {X : Scheme.{u}} (p : X ⟶ Spec (.of R)) [IsProper p]
    (Z : Closeds X) (hZ : Z ≤ (baseIdealSheaf R (IsLocalRing.maximalIdeal R) p).support)
    (U : X.Opens) (hU : (U : Set X) = (Z : Set X)ᶜ)
    (F : Stacks.Coherent.CoherentAdicSystems
      ((baseIdealSheaf R (IsLocalRing.maximalIdeal R) p).comap U.ι))
    (hflat : ∀ n : ℕ, StalksFlatOverQuotient R (baseToStalk R (U.ι ≫ p))
      (IsLocalRing.maximalIdeal R ^ (n + 1)) (F.obj.obj (op n)))
    (h0 : ((Scheme.Modules.pushforward U.ι).obj (F.obj.obj (op 0))).IsCoherent)
    (h1 : (((Scheme.Modules.pushforward U.ι).rightDerived 1).obj (F.obj.obj (op 0))).IsCoherent) :
    letI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian p
    IsCompletionOfCoherent ((baseIdealSheaf R (IsLocalRing.maximalIdeal R) p).comap U.ι) F

Stacks.Algebraization.exists_specialFibre_directImage_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/SpecialFibreDirectImages.lean, line 116. The attribute's comment: “the closing paragraph: F₁ is a coherent sheaf on the special fibre U₁, and j_F₁ = j₁,F₁ and R¹j_F₁ = R¹j₁,F₁ for the special fibre j₁ : U₁ → X₁ of j”.

Stacks 0EJV, the closing paragraph: j_*F_1 and R¹j_*F_1 are conditions on the special fibre. Let (R, 𝔪) be a Noetherian local ring, p : X ⟶ Spec R proper, U ⊆ X open with inclusion j, and (F_n) an object of Coh(U, 𝔪𝒪_U). Write i : X_1 ⟶ X and i_U : U_1 ⟶ U for the special fibres and j₁ : U_1 ⟶ X_1 for the special fibre of j. Then F_1 is a coherent sheaf on U_1: there is a coherent 𝒪_{U_1}-module G with i_{U,*} G ≅ F_1; and j_*F_1 ≅ i_* j₁_* G and R¹j_*F_1 ≅ i_* R¹j₁_* G.

theorem exists_specialFibre_directImage_iso
    (R : Type u) [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    {X : Scheme.{u}} (p : X ⟶ Spec (.of R)) [IsProper p] (U : X.Opens)
    (F : Stacks.Coherent.CoherentAdicSystems
      ((baseIdealSheaf R (IsLocalRing.maximalIdeal R) p).comap U.ι)) :
    ∃ G : ((baseIdealSheaf R (IsLocalRing.maximalIdeal R) p).comap U.ι).subscheme.Modules,
      G.IsCoherent ∧
      Nonempty ((Scheme.Modules.pushforward
        ((baseIdealSheaf R (IsLocalRing.maximalIdeal R) p).comap U.ι).subschemeι).obj G ≅
          F.obj.obj (op 0)) ∧
      Nonempty ((Scheme.Modules.pushforward U.ι).obj (F.obj.obj (op 0)) ≅
        (Scheme.Modules.pushforward
          (baseIdealSheaf R (IsLocalRing.maximalIdeal R) p).subschemeι).obj
          ((Scheme.Modules.pushforward
            (specialFibreMap (baseIdealSheaf R (IsLocalRing.maximalIdeal R) p) U)).obj G)) ∧
      Nonempty (((Scheme.Modules.pushforward U.ι).rightDerived 1).obj (F.obj.obj (op 0)) ≅
        (Scheme.Modules.pushforward
          (baseIdealSheaf R (IsLocalRing.maximalIdeal R) p).subschemeι).obj
          (((Scheme.Modules.pushforward
            (specialFibreMap (baseIdealSheaf R (IsLocalRing.maximalIdeal R) p) U)).rightDerived
              1).obj G))

Stacks.Algebraization.isCoherent_specialFibre_directImages_of_hasPropertySk_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizationCoherentFormal/SpecialFibreSerreCriterion.lean, line 255. The attribute's comment: “the closing paragraph: if X₁ is (S₂) and irreducible, dim(X₁) - dim(Z) ≥ 3 and F₁ is a locally free O_{U₁}-module, then j₁,F₁ and R¹j₁,F₁ are coherent”.

Stacks 0EJV, the closing paragraph: the (S₂) criterion on the special fibre. Let (R, 𝔪) be a Noetherian local ring, p : X ⟶ Spec R locally of finite type, Z ⊆ X closed and U = X ∖ Z. Write X₁ and U₁ for the special fibres and j₁ : U₁ ⟶ X₁ for the special fibre of the inclusion U ⊆ X. If X₁ is (S₂) and irreducible, dim(X₁) - dim(Z) ≥ 3, and G is a finite locally free 𝒪_{U₁}-module, then j₁,*G and R¹j₁,*G are coherent.

The special fibre is locally of finite type over the residue field R/𝔪, being the base change X ×_{Spec R} Spec(R/𝔪) (Stacks.PuncturedSpectrumPicard.baseIdealSubschemeIsoPullback); j₁ is an open immersion whose image is X₁ ∖ Z; and the closed subset X₁ ∩ Z of X₁ has dimension at most dim(Z). So Stacks.Algebraization.isCoherent_pushforward_and_rightDerived_one_of_hasPropertySk_two applies.

theorem isCoherent_specialFibre_directImages_of_hasPropertySk_two
    (R : Type u) [CommRing R] [IsNoetherianRing R] [IsLocalRing R]
    {X : Scheme.{u}} (p : X ⟶ Spec (.of R)) [LocallyOfFiniteType p]
    (Z : Closeds X) (U : X.Opens) (hU : (U : Set X) = (Z : Set X)ᶜ)
    [IrreducibleSpace (baseIdealSheaf R (IsLocalRing.maximalIdeal R) p).subscheme]
    (hS₂ : letI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian p
      letI : IsLocallyNoetherian (baseIdealSheaf R (IsLocalRing.maximalIdeal R) p).subscheme :=
        isLocallyNoetherian_of_isClosedImmersion
          (baseIdealSheaf R (IsLocalRing.maximalIdeal R) p).subschemeι
      HasPropertySk (baseIdealSheaf R (IsLocalRing.maximalIdeal R) p).subscheme 2)
    (hdim : topologicalKrullDim (Z : Set X) + 3 ≤
      topologicalKrullDim (baseIdealSheaf R (IsLocalRing.maximalIdeal R) p).subscheme)
    (G : ((baseIdealSheaf R (IsLocalRing.maximalIdeal R) p).comap U.ι).subscheme.Modules)
    (hG : Scheme.Modules.IsFiniteLocallyFree G) :
    ((Scheme.Modules.pushforward
        (specialFibreMap (baseIdealSheaf R (IsLocalRing.maximalIdeal R) p) U)).obj G).IsCoherent ∧
      (((Scheme.Modules.pushforward
        (specialFibreMap (baseIdealSheaf R (IsLocalRing.maximalIdeal R) p) U)).rightDerived
          1).obj G).IsCoherent

Sources

• Section 52.23, Tag 0EJR
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Algebraization.finite_globalSections_of_finite_idealPowerSections · Stacks.Algebraization.canonicallyExtends_of_finite_globalSections · Stacks.Algebraization.canonicallyExtends_of_finite_idealPowerSections · Stacks.Algebraization.HasRegularSequenceOnCompletedStalks · Stacks.Algebraization.HasFiniteLowDegreeCohomology · Stacks.Algebraization.canonicallyExtends_of_regularSequence · Stacks.Algebraization.essImage_completionFunctor_of_regularSequence · Stacks.Algebraization.hasFiniteLowDegreeCohomology_iff_hasDepthDimensionAt_two

Section52.24 Application to the completion functor#

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

Tag 0EKY, a lemma

Tag 0EKY in the Stacks Project.

Stacks.Algebraization.completionEquivalence_local_principal_finiteLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionCriteria/LocalPrincipalEquivalence.lean, line 489.

[Stacks, Tag 0EKY]. In Situation 0EHC assume

1. A has a dualizing complex and is I-adically complete,
2. I = (f) is generated by a single element,
3. A is local with maximal ideal 𝔞 = 𝔪,
4. one of the following is true
5. (a) A_f is (S₂) and for 𝔭 ⊂ A minimal with f ∉ 𝔭 we have dim(A/𝔭) ≥ 4, or
6. (b) if 𝔭 ∉ V(f) and V(𝔭) ∩ V(f) ≠ {𝔪}, then depth(A_𝔭) + dim(A/𝔭) > 3.

Then with U₀ = U ∩ V(f) the completion functor colim_{U₀ ⊆ U' ⊆ U open} Coh(𝒪_{U'}) ⟶ Coh(U, f𝒪_U) is an equivalence on the full subcategories of finite locally free objects. As for [Stacks, Tag 0EKZ] (Stacks.Algebraization.completionEquivalence_principal_finiteLocallyFree), this is three statements, and they are the three conjuncts below:

1. the functor carries a finite locally free coherent module on an open neighbourhood V of U₀ inside U to a finite locally free object of Coh(V, f𝒪_V). At the member V = U the stalkwise form of that conclusion holds too;
2. it is fully faithful there: for every open neighbourhood V of U₀ inside U and all finite locally free 𝒪_V-modules 𝒢, ℱ the canonical map colim_{V' ⊆ V} Hom_{V'}(𝒢|_{V'}, ℱ|_{V'}) ⟶ Hom_{Coh(V, f𝒪_V)}(𝒢^∧, ℱ^∧) is bijective;
3. it is essentially surjective onto them: every finite locally free object of Coh(U, f𝒪_U) is the completion of a finite locally free coherent module on some open neighbourhood of U₀ inside U.

An object of colim_{U₀ ⊆ U' ⊆ U} Coh(𝒪_{U'}) is a coherent module on one of the neighbourhoods, so the first two conjuncts quantify over a neighbourhood. Two objects given on V₁ and V₂ are compared on V₁ ∩ V₂, which is again a neighbourhood. The target of the second conjunct is Coh(U, f𝒪_U) on morphisms (Stacks.Algebraization.bijective_restrictCompletionHom). A finite locally free object is one whose n-th term is a finite locally free 𝒪/fⁿ⁺¹𝒪-module: in the first conjunct this is Stacks.Algebraization.IsFiniteLocallyFreeAdic, and in the third its stalkwise content Stacks.Algebraization.HasFiniteFreeStalks, which the first conjunct also delivers. So the conjuncts compose into the equivalence.

Hypothesis (4a) reads "A_f is (S₂)" as PropertySkRing (Localization.Away f) 2, Serre's condition of [Stacks, Tag 031P] for the ring A_f. In (4b), V(f) is the set of primes containing f.

The source's proof: full faithfulness is [Stacks, Tag 0EKU] (completionFullyFaithful_finiteLocallyFree_of_isLocalRing_of_eq_span_singleton). Essential surjectivity is [Stacks, Tag 0EJ9] fed by [Stacks, Tag 0EJB], followed by the passage to the locus where the module is free (isCompletionNearClosedFiniteLocallyFree_of_isLocalRing_of_eq_span_singleton).

theorem completionEquivalence_local_principal_finiteLocallyFree
    [IsLocalRing S.A] {f : S.A} [HasDerivedCategory.{w} (ModuleCat.{u} S.A)]
    (hdual : ∃ K : DerivedCategory (ModuleCat.{u} S.A), Dualizing.IsDualizingComplex K)
    (hcomplete : IsAdicComplete S.I S.A)
    (hI : S.I = Ideal.span {f})
    (hmax : S.a = maximalIdeal S.A)
    (hcond :
      (PropertySkRing (Localization.Away f) 2 ∧
        ∀ p : PrimeSpectrum S.A, IsMinimalPrime p.asIdeal → f ∉ p.asIdeal →
          (4 : WithBot ℕ∞) ≤ ringKrullDim (S.A ⧸ p.asIdeal)) ∨
      (∀ p : PrimeSpectrum S.A, f ∉ p.asIdeal →
        ({q : PrimeSpectrum S.A | p.asIdeal ≤ q.asIdeal} ∩
          {q : PrimeSpectrum S.A | f ∈ q.asIdeal}) ≠
          {⟨maximalIdeal S.A, (maximalIdeal.isMaximal S.A).isPrime⟩} →
        (3 : WithBot ℕ∞) <
          (Module.depth (Localization.AtPrime p.asIdeal)
            (maximalIdeal (Localization.AtPrime p.asIdeal))
            (Localization.AtPrime p.asIdeal) : WithBot ℕ∞) +
            ringKrullDim (S.A ⧸ p.asIdeal))) :
    ((∀ (V : S.U.toScheme.Opens),
          (S.U.ι.base ⁻¹' Set.range S.Yι.base) ⊆ (V : Set S.U.toScheme) →
          ∀ G : AlgebraicGeometry.SheafOfModules.CoherentModules V.toScheme.ringCatSheaf,
            AlgebraicGeometry.Scheme.Modules.IsFiniteLocallyFree G.obj →
            IsFiniteLocallyFreeAdic ((idealOnOpen S).comap V.ι)
              ((completionFunctor V.toScheme ((idealOnOpen S).comap V.ι)).obj G)) ∧
        ∀ G : AlgebraicGeometry.SheafOfModules.CoherentModules S.U.toScheme.ringCatSheaf,
          AlgebraicGeometry.Scheme.Modules.IsFiniteLocallyFree G.obj →
          HasFiniteFreeStalks S ((completionFunctor S.U.toScheme (idealOnOpen S)).obj G)) ∧
      (∀ (V : OpensNearVanishing S.A S.I S.a)
        (G F : AlgebraicGeometry.SheafOfModules.CoherentModules V.openSet.toScheme.ringCatSheaf),
        Scheme.Modules.IsFiniteLocallyFree G.obj → Scheme.Modules.IsFiniteLocallyFree F.obj →
          Function.Bijective (nbhdHomComparisonOn V G F)) ∧
      (∀ F : Stacks.Coherent.CoherentAdicSystems (idealOnOpen S),
        HasFiniteFreeStalks S F → IsCompletionNearClosedFiniteLocallyFree S F)

Tag 0EKZ, a lemma

Tag 0EKZ in the Stacks Project.

Stacks.Algebraization.completionEquivalence_principal_finiteLocallyFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionCriteria/PrincipalEquivalence.lean, line 495.

[Stacks, Tag 0EKZ]. Let S be the standing situation of [Stacks, Tag 0EHC] and write U₀ = U ∩ V(f). Assume

1. I = (f) is a principal ideal,
2. A is complete with respect to the f-adic topology,
3. f is a nonzerodivisor of A, and
4. H¹_𝔞(A/fA) and H²_𝔞(A/fA) are finite A-modules.

Then the completion functor colim_{U₀ ⊆ U' ⊆ U} Coh(𝒪_{U'}) ⟶ Coh(U, f𝒪_U) restricts to an equivalence on the full subcategories of finite locally free objects. Elementwise this is three statements, and they are the three conjuncts below:

1. the functor carries a finite locally free coherent module on an open neighbourhood V of U₀ inside U to a finite locally free object of Coh(V, f𝒪_V), and — at the member V = U of 𝒱 — the stalkwise form of that conclusion;
2. it is fully faithful there: for every open neighbourhood V of U₀ inside U and all finite locally free 𝒪_V-modules 𝒢, ℱ the canonical map colim_{U₀ ⊆ W ⊆ V} Hom_{W}(𝒢|_{W}, ℱ|_{W}) ⟶ Hom_{Coh(U, f𝒪_U)}(𝒢^∧, ℱ^∧) is bijective;
3. it is essentially surjective onto them: every finite locally free object of Coh(U, f𝒪_U) is the completion of a finite locally free coherent module on some open neighbourhood of U₀ inside U.

The objects of colim_{U₀ ⊆ U' ⊆ U} Coh(𝒪_{U'}) are the coherent modules on the individual neighbourhoods, so the second conjunct quantifies over a neighbourhood V and a pair of finite locally free modules on it, and renders Hom_{Coh(U, f𝒪_U)}(𝒢^∧, ℱ^∧) as the inverse limit of the morphisms 𝒢|_{U₀,n} ⟶ ℱ|_{U₀,n} over the infinitesimal neighbourhoods of U₀, which is what a morphism of the two inverse systems 𝒢^∧, ℱ^∧ is. That is Stacks.Algebraization.NeighbourhoodCompletion.CompletionFullyFaithfulComplete.

A finite locally free object of Coh(V, ℐ) is, by the source's own definition, one whose n-th term is a finite locally free 𝒪_V/ℐ^{n+1}-module. A term of a coherent adic system is annihilated by ℐ^{n+1}, so over 𝒪_V itself the only finite locally free such term is zero; the condition has to be read over the closed subscheme cut out by ℐ^{n+1}, and that is Stacks.Algebraization.IsFiniteLocallyFreeAdic — the n-th term is the direct image of a finite locally free module on that subscheme. This is the form the first conjunct takes, for a module defined on an arbitrary member V of 𝒱, the objects of colim_𝒱 Coh(𝒪_V) being the coherent modules on the individual neighbourhoods. Its second half is the same conclusion read at the stalks at the member V = U, namely Stacks.Algebraization.HasFiniteFreeStalks; that is the hypothesis the third conjunct consumes, so the two halves together let the three conjuncts compose into the equivalence. The quantification is not vacuous: V = ⊤ is a member of 𝒱.

The source's proof is two citations: full faithfulness is [Stacks, Tag 0EKV], which is Stacks.Algebraization.completionFullyFaithfulComplete_principal, and essential surjectivity is [Stacks, Tag 0DXW], which is Stacks.Algebraization.canonicallyExtends_and_isCompletion_of_principal. The first conjunct is the statement that the functor lands in the finite locally free objects, by Stacks.Algebraization.isFiniteLocallyFreeAdic_completion and Stacks.Algebraization.hasFiniteFreeStalks_completionFunctor_of_isFiniteLocallyFree, and the finite local freeness of the module produced in the third is obtained by shrinking the neighbourhood to the locus where it is free.

theorem completionEquivalence_principal_finiteLocallyFree {f : S.A}
    (hI : S.I = Ideal.span {f}) (hcomplete : IsAdicComplete (Ideal.span {f}) S.A)
    (hnzd : f ∈ nonZeroDivisors S.A)
    (hH1 : Module.Finite S.A (specialFibreLocalCohomology S f 1))
    (hH2 : Module.Finite S.A (specialFibreLocalCohomology S f 2)) :
    ((∀ (V : S.U.toScheme.Opens),
          (S.U.ι.base ⁻¹' Set.range S.Yι.base) ⊆ (V : Set S.U.toScheme) →
          ∀ G : AlgebraicGeometry.SheafOfModules.CoherentModules V.toScheme.ringCatSheaf,
            AlgebraicGeometry.Scheme.Modules.IsFiniteLocallyFree G.obj →
            IsFiniteLocallyFreeAdic ((idealOnOpen S).comap V.ι)
              ((completionFunctor V.toScheme ((idealOnOpen S).comap V.ι)).obj G)) ∧
        ∀ G : AlgebraicGeometry.SheafOfModules.CoherentModules S.U.toScheme.ringCatSheaf,
          AlgebraicGeometry.Scheme.Modules.IsFiniteLocallyFree G.obj →
          HasFiniteFreeStalks S ((completionFunctor S.U.toScheme (idealOnOpen S)).obj G)) ∧
      NeighbourhoodCompletion.CompletionFullyFaithfulComplete
        (principalFormalLocusι S.A S.a f) ∧
      (∀ F : Stacks.Coherent.CoherentAdicSystems (idealOnOpen S),
        HasFiniteFreeStalks S F → IsCompletionNearClosedFiniteLocallyFree S F)

Stacks.Algebraization.isCompletionNearClosed_of_principal_shortExactSequences, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionCriteria/PrincipalNonzerodivisor.lean, line 608. The attribute's comment: “the essential-surjectivity half: over an f-adically complete A, a coherent I-adic system on U which has the short exact sequences 0 → Fₙ → F₍ₙ₊₁₎ → F₁ → 0 of the proof of Stacks 0DXW and whose H⁰(U, F₁) and H¹(U, F₁) are finite is the completion of a coherent module on an open neighbourhood of U ∩ V(f) in U, i.e. lies in the image of the colimit functor of this tag. Those two properties of the system are what the proof of Stacks 0DXW draws from its conditions (2) and (3), and they are what is asked for here in their place. This declaration does not cover full faithfulness, which is Stacks 0EKV; and finite local freeness of the module produced, and so its invertibility, is not among its conclusions, which give coherence alone — all that the final clause of Stacks 0DXW gives as well”.

Stacks Project, Tag 0EKZ, the essential-surjectivity half. Let S be an algebraization situation whose ideal I is generated by f ∈ A, let A be f-adically complete, and let (F_n) be a coherent I-adic system on the open complement U. If the system has the short exact sequences 0 → F_n → F_{n+1} → F_1 → 0 of the proof of Stacks 0DXW and if H⁰(U, F_1) and H¹(U, F_1) are finite A-modules, then (F_n) is the completion of a coherent module on an open neighbourhood of U ∩ V(f) inside U: it lies in the image of the completion functor colim_{U₀ ⊆ U' ⊆ U} Coh(𝒪_{U'}) ⟶ Coh(U, f𝒪_U) of Stacks 0EKZ.

The system extends canonically to X by Stacks 0DXW, and part (2) of Stacks 0EIR turns that into extendability. Adic completeness then runs the chain of Stacks 0EIL: an extendable system is the restriction of a completion on X, hence the completion of a module restricted from X, hence a completion on U, hence a completion near the closed subscheme.

Two properties of the system are asked for in place of conditions (2) and (3) of Stacks 0DXW, being what its proof draws from them, exactly as in Stacks.Algebraization.canonicallyExtends_of_principal_shortExactSequences. The full-faithfulness half of Stacks 0EKZ is Stacks 0EKV, and the module produced here is coherent, with finite local freeness not among the conclusions.

Stacks 0EKZ itself, with the source's own hypotheses and all of its content, is Stacks.Algebraization.completionEquivalence_principal_finiteLocallyFree, which derives the two hypotheses below from them and produces a finite locally free module.

theorem isCompletionNearClosed_of_principal_shortExactSequences (f : S.A)
    (hI : S.I = Ideal.span {f}) (hcomplete : IsAdicComplete (Ideal.span {f}) S.A)
    (h : HasPrincipalShortExactSequences S F f)
    (h0 : Module.Finite S.A ((globalSectionsSystem S F).obj (op 0)))
    (h1 : Module.Finite S.A ((openCohomologyFunctor S 1).obj (systemObj S F 0))) :
    IsCompletionNearClosed S (kerComapSystem S F)

Sources

• Section 52.24, Tag 0EKX
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Algebraization.completionEquivalence_local_principal_finiteLocallyFree · Stacks.Algebraization.completionEquivalence_principal_finiteLocallyFree · Stacks.Algebraization.isCompletionNearClosed_of_principal_shortExactSequences

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.