52.25 Coherent triples to 52.28 Application to Lefschetz…

Section52.25 Coherent triples #

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

Tag 0F23, a lemma

Tag 0F23 in the Stacks Project.

Stacks.Algebraization.nonempty_preparedExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/CoherentTriplePreparation.lean, line 262.

Stacks Project, Tag 0F23. Every coherent triple admits a prepared extension: a coherent module on Spec A on which f acts regularly, isomorphic to the triple's punctured-spectrum member over the punctured spectrum, and mapping compatibly to its closed-fibre member.

The module is 𝔪ⁿ G for a coherent extension G ⟶ j_*F of the punctured-spectrum member of the triple and a suitable power n; the three steps are described in the implementation notes of this file.

public theorem nonempty_preparedExtension (A : Type u) [CommRing A]
    [IsLocalRing A] [IsNoetherianRing A] (f : A) (hf : f ∈ IsLocalRing.maximalIdeal A)
    (hreg : IsRegular f) (T : CoherentTriple A f) : Nonempty (PreparedExtension A f T)

Tag 0F24, an equation

Tag 0F24 in the Stacks Project.

Stacks.Algebraization.CoherentTriple.eulerCharacteristic, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/CoherentTripleHilbertPolynomial.lean, line 92. The attribute's comment: “the Euler characteristic of the triple itself”.

The Euler characteristic of a coherent triple: the length of the cokernel minus the length of the kernel of the closed-fibre map of a prepared extension. Prepared extensions exist by Stacks.Algebraization.nonempty_preparedExtension, and the number does not depend on the one chosen by Stacks.Algebraization.PreparedExtension.eulerCharacteristic_eq.

public noncomputable def CoherentTriple.eulerCharacteristic {A : Type u} [CommRing A]
    [IsLocalRing A] [IsNoetherianRing A] {f : A} (hf : f ∈ IsLocalRing.maximalIdeal A)
    (hreg : IsRegular f) (T : CoherentTriple A f) : ℤ

Stacks.Algebraization.kernel_finiteLength, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/CoherentTripleLength.lean, line 490. The attribute's comment: “finite length of the kernel”.

The kernel of the closed-fibre map of a prepared extension has finite length over A.

public theorem kernel_finiteLength
    (A : Type u) [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    (f : A)
    (T : CoherentTriple A f) (P : PreparedExtension A f T) :
    IsFiniteLength A (kernel P.closedFibreMap).carrier

Stacks.Algebraization.cokernel_finiteLength, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/CoherentTripleLength.lean, line 503. The attribute's comment: “finite length of the cokernel”.

The cokernel of the closed-fibre map of a prepared extension has finite length over A.

public theorem cokernel_finiteLength
    (A : Type u) [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    (f : A)
    (T : CoherentTriple A f) (P : PreparedExtension A f T) :
    IsFiniteLength A (cokernel P.closedFibreMap).carrier

Tag 0F25, a lemma

Tag 0F25 in the Stacks Project.

Stacks.Algebraization.PreparedExtension.eulerCharacteristic_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/CoherentTripleEulerCharacteristic/WellDefined.lean, line 483.

Stacks Project, Tag 0F25. The Euler characteristic of a coherent triple does not depend on the prepared extension used to compute it: any two prepared extensions of the same triple have the same Euler characteristic.

public theorem PreparedExtension.eulerCharacteristic_eq
    (A : Type u) [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    (f : A) (hf : f ∈ IsLocalRing.maximalIdeal A)
    (T : CoherentTriple A f) (P Q : PreparedExtension A f T) :
    P.eulerCharacteristic = Q.eulerCharacteristic

Tag 0F26, a lemma

Tag 0F26 in the Stacks Project.

Stacks.Algebraization.eulerCharacteristic_add_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/CoherentTripleEulerCharacteristic/Additivity.lean, line 727.

Stacks Project, Tag 0F26. The Euler characteristic of a coherent triple is additive along a short exact sequence of coherent triples: for any prepared extensions P, Q and N of the three terms, the Euler characteristic of Q is the sum of those of P and N.

public theorem eulerCharacteristic_add_of_shortExact
    (A : Type u) [CommRing A] [IsLocalRing A] [IsNoetherianRing A] (f : A)
    (hf : f ∈ IsLocalRing.maximalIdeal A)
    {T S R : CoherentTriple A f} {φ : T.Hom S} {ψ : S.Hom R}
    (hT : CoherentTriple.ShortExact φ ψ)
    (P : PreparedExtension A f T) (Q : PreparedExtension A f S)
    (N : PreparedExtension A f R) :
    Q.eulerCharacteristic = P.eulerCharacteristic + N.eulerCharacteristic

Stacks.Algebraization.CoherentTriple.eulerCharacteristic_add_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/CoherentTripleHilbertPolynomial.lean, line 158. The attribute's comment: “additivity for the Euler characteristics of the triples themselves”.

Stacks Project, Tag 0F26 for the triples themselves. The Euler characteristic of a coherent triple is additive along a short exact sequence of coherent triples.

public theorem CoherentTriple.eulerCharacteristic_add_of_shortExact {A : Type u} [CommRing A]
    [IsLocalRing A] [IsNoetherianRing A] {f : A} (hf : f ∈ IsLocalRing.maximalIdeal A)
    (hreg : IsRegular f) {T S R : CoherentTriple A f} {φ : CoherentTriple.Hom T S}
    {ψ : CoherentTriple.Hom S R} (hse : CoherentTriple.ShortExact φ ψ) :
    S.eulerCharacteristic hf hreg =
      T.eulerCharacteristic hf hreg + R.eulerCharacteristic hf hreg

Tag 0F27, a proposition

Tag 0F27 in the Stacks Project.

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

Let A be a Noetherian local ring, f ∈ 𝔪 a nonzerodivisor, and (L, L₀, λ) an invertible coherent triple. For every coherent triple T = (F, F₀, α) there is a polynomial P ∈ ℚ[t] with

χ(T ⊗ (L, L₀, λ)^{⊗ n}) = P(n) for every n ∈ ℤ,

and deg P ≤ dim(Supp F), the dimension being truncated at 0.

public theorem exists_polynomial_natDegree_le_dim_supp (hf : f ∈ maximalIdeal A)
    (hreg : IsRegular f) (L : CoherentTriple A f) (hL : IsInvertibleTriple L)
    (T : CoherentTriple A f) :
    ∃ P : Polynomial ℚ,
      (P.natDegree : WithBot ℕ∞) ≤ max 0 (topologicalKrullDim ↥(SheafOfModules.supp T.F)) ∧
        ∀ n : ℤ, (((T.twistZ L hL n).eulerCharacteristic hf hreg : ℤ) : ℚ) = P.eval (n : ℚ)

Stacks.Algebraization.exists_polynomial_natDegree_le_of_forall_sub_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/CoherentTripleHilbertPolynomial.lean, line 207. The attribute's comment: “the concluding step: polynomiality on ℤ from the first difference”.

A function on all of ℤ whose first difference is a polynomial is a polynomial. If g : ℤ → ℤ satisfies g (n + 1) - g n = Q(n) at every integer n, with Q a rational polynomial of degree at most d, then g agrees at every integer with a rational polynomial of degree at most d + 1.

This is the variant of [Stacks, Tag 00JZ] for functions defined on all integers with which the proof of [Stacks, Tag 0F27] concludes, and unlike IsNumericalPolynomial it constrains the function at every integer rather than only at large ones.

public theorem exists_polynomial_natDegree_le_of_forall_sub_eq {g : ℤ → ℤ} {d : ℕ}
    {Q : Polynomial ℚ} (hQ : Q.natDegree ≤ d)
    (hg : ∀ n : ℤ, (g (n + 1) : ℚ) - (g n : ℚ) = Q.eval (n : ℚ)) :
    ∃ P : Polynomial ℚ, P.natDegree ≤ d + 1 ∧ ∀ n : ℤ, (g n : ℚ) = P.eval (n : ℚ)

Stacks.Algebraization.CoherentTriple.twistPow, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/CoherentTripleTensor.lean, line 246. The attribute's comment: “the twist of a coherent triple by the nonnegative powers of an invertible triple”.

The twists of a coherent triple by the nonnegative tensor powers of an invertible coherent triple. The zeroth twist is the triple itself and each further one is the tensor product of the previous one with the invertible triple, so the n-th is (F ⊗ L^\{⊗ n}, F₀ ⊗ L₀^\{⊗ n}, α ⊗ λ^\{⊗ n}) up to the associativity of the tensor product. This is the family whose Euler characteristics [Stacks, Tag 0F27] asserts to be given by a polynomial.

public noncomputable def CoherentTriple.twistPow {A : Type u} [CommRing A] [IsLocalRing A]
    {f : A} (T L : CoherentTriple A f) (hL : IsInvertibleTriple L) : ℕ → CoherentTriple A f

Stacks.Algebraization.CoherentTriple.twistZ, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/CoherentTripleTwist.lean, line 187. The attribute's comment: “the integer twists of a coherent triple by an invertible coherent triple”.

The twist of a coherent triple by the n-th tensor power of an invertible coherent triple, for n : ℤ. Its members are the tensor products of the members of the triple with the n-th tensor powers of the members of the invertible triple, and its identification over the punctured closed fibre is the tensor product of the two identifications, the second taken in its n-th tensor power.

This is the family whose Euler characteristics [Stacks, Tag 0F27] asserts to be given by a polynomial.

public noncomputable def CoherentTriple.twistZ {A : Type u} [CommRing A] [IsLocalRing A] {f : A}
    (T L : CoherentTriple A f) (hL : IsInvertibleTriple L) (n : ℤ) : CoherentTriple A f

Tag 0F28, a lemma

Tag 0F28 in the Stacks Project.

Stacks.Algebraization.CoherentTriple.eulerCharacteristic_eq_length_cokernel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/CoherentTripleEulerFormula.lean, line 168. The attribute's comment: “the Euler characteristic formula”.

Stacks Project, Tag 0F28. For an invertible coherent triple over a Noetherian local ring of depth at least three, the Euler characteristic of the triple is the length of the cokernel of the canonical map on global sections.

The prepared extension taken is the direct image of the triple's punctured-spectrum member; its closed-fibre map has a cokernel of the same length as that of the canonical map on global sections, and its kernel vanishes because the global sections of that direct image have depth at least two over A.

public theorem CoherentTriple.eulerCharacteristic_eq_length_cokernel (A : Type u) [CommRing A]
    [IsLocalRing A] [IsNoetherianRing A] (f : A) (hf : f ∈ maximalIdeal A) (hreg : IsRegular f)
    (T : CoherentTriple A f)
    [AlgebraicGeometry.SheafOfModules.IsInvertible
      (Stacks.Divisors.puncturedSpectrum A).toScheme.presheaf
      (Stacks.Divisors.puncturedSpectrum A).toScheme.ringCatSheaf.2 T.F]
    [AlgebraicGeometry.SheafOfModules.IsInvertible (closedFibre A f).presheaf
      (closedFibre A f).ringCatSheaf.2 T.F₀]
    (hdepth : 3 ≤ Module.depth A (maximalIdeal A) A) :
    letI := puncturedSectionsModule A T.F
    letI := puncturedClosedFibreSectionsModule A f
      ((Scheme.Modules.pullback (puncturedClosedFibre A f).ι).obj T.F₀)
    T.eulerCharacteristic hf hreg =
      ((Module.length A
        (Γ((Scheme.Modules.pullback (puncturedClosedFibre A f).ι).obj T.F₀, ⊤) ⧸
          LinearMap.range (globalSectionsMap A f T))).toNat : ℤ)

Stacks.Algebraization.CoherentTriple.eulerCharacteristic_nonneg, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/CoherentTripleEulerFormula.lean, line 210. The attribute's comment: “nonnegativity”.

The Euler characteristic of an invertible coherent triple is nonnegative, being the length of a cokernel.

public theorem CoherentTriple.eulerCharacteristic_nonneg (A : Type u) [CommRing A]
    [IsLocalRing A] [IsNoetherianRing A] (f : A) (hf : f ∈ maximalIdeal A) (hreg : IsRegular f)
    (T : CoherentTriple A f)
    [AlgebraicGeometry.SheafOfModules.IsInvertible
      (Stacks.Divisors.puncturedSpectrum A).toScheme.presheaf
      (Stacks.Divisors.puncturedSpectrum A).toScheme.ringCatSheaf.2 T.F]
    [AlgebraicGeometry.SheafOfModules.IsInvertible (closedFibre A f).presheaf
      (closedFibre A f).ringCatSheaf.2 T.F₀]
    (hdepth : 3 ≤ Module.depth A (maximalIdeal A) A) :
    0 ≤ T.eulerCharacteristic hf hreg

Stacks.Algebraization.globalSectionsMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/CoherentTripleInvertible.lean, line 170. The attribute's comment: “the canonical map on global sections”.

The canonical map on global sections of a coherent triple. It carries a section of the module on the punctured spectrum to its restriction to the punctured closed fibre, read through the triple's identification as a section of the module on the closed fibre. It is linear over A, which acts on both sides through the structure morphisms.

noncomputable def globalSectionsMap (A : Type u) [CommRing A] [IsLocalRing A] (f : A)
    (T : CoherentTriple A f) :
    letI := puncturedSectionsModule A T.F
    letI := puncturedClosedFibreSectionsModule A f
      ((Scheme.Modules.pullback (puncturedClosedFibre A f).ι).obj T.F₀)
    Γ(T.F, ⊤) →ₗ[A] Γ((Scheme.Modules.pullback (puncturedClosedFibre A f).ι).obj T.F₀, ⊤)

Stacks.Algebraization.finiteLength_cokernel_globalSectionsMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/CoherentTripleInvertible.lean, line 751. The attribute's comment: “finite length of the cokernel”.

The cokernel of the canonical map on global sections has finite length. The restriction map from the closed fibre to the punctured closed fibre is surjective, by Hartogs extension on A / fA, and restriction along the closed immersion is surjective on global sections, so the cokernel is a quotient of the cokernel of the closed-fibre map of any prepared extension of the triple, which has finite length.

theorem finiteLength_cokernel_globalSectionsMap (A : Type u) [CommRing A] [IsLocalRing A]
    [IsNoetherianRing A] (f : A) (hf : f ∈ maximalIdeal A) (hreg : IsRegular f)
    (T : CoherentTriple A f)
    [AlgebraicGeometry.SheafOfModules.IsInvertible (closedFibre A f).presheaf
      (closedFibre A f).ringCatSheaf.2 T.F₀]
    (hdepth : 3 ≤ Module.depth A (maximalIdeal A) A) :
    letI := puncturedSectionsModule A T.F
    letI := puncturedClosedFibreSectionsModule A f
      ((Scheme.Modules.pullback (puncturedClosedFibre A f).ι).obj T.F₀)
    IsFiniteLength A
      (Γ((Scheme.Modules.pullback (puncturedClosedFibre A f).ι).obj T.F₀, ⊤) ⧸
        LinearMap.range (globalSectionsMap A f T))

Stacks.Algebraization.CoherentTriple.eulerCharacteristic_eq_zero_iff_isTrivial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/CoherentTripleTriviality.lean, line 316. The attribute's comment: “vanishing criterion”.

Stacks Project, Tag 0F28. For an invertible coherent triple over a Noetherian local ring of depth at least three, the Euler characteristic of the triple vanishes exactly when the member on the punctured spectrum is trivial.

By the Euler-characteristic formula the vanishing is the surjectivity of the canonical map on global sections, which for the prepared extension given by the direct image of the punctured-spectrum member is the surjectivity of the closed-fibre map; that map is injective by Stacks.Algebraization.injective_closedFibreMap_of_pushforward, and the two halves of the criterion are Stacks.Algebraization.isTrivial_of_bijective_closedFibreMap and Stacks.Algebraization.isIso_closedFibreMap_of_isTrivial.

public theorem CoherentTriple.eulerCharacteristic_eq_zero_iff_isTrivial (A : Type u) [CommRing A]
    [IsLocalRing A] [IsNoetherianRing A] (f : A) (hf : f ∈ maximalIdeal A) (hreg : IsRegular f)
    (T : CoherentTriple A f)
    [AlgebraicGeometry.SheafOfModules.IsInvertible
      (Stacks.Divisors.puncturedSpectrum A).toScheme.presheaf
      (Stacks.Divisors.puncturedSpectrum A).toScheme.ringCatSheaf.2 T.F]
    [AlgebraicGeometry.SheafOfModules.IsInvertible (closedFibre A f).presheaf
      (closedFibre A f).ringCatSheaf.2 T.F₀]
    (hdepth : 3 ≤ Module.depth A (maximalIdeal A) A) :
    T.eulerCharacteristic hf hreg = 0 ↔
      Stacks.SheafOfModules.IsTrivial (Stacks.Divisors.puncturedSpectrum A).toScheme.presheaf
        (Stacks.Divisors.puncturedSpectrum A).toScheme.ringCatSheaf.2 T.F

Sources

LeanStacks.Algebraization.nonempty_preparedExtension · Stacks.Algebraization.CoherentTriple.eulerCharacteristic · Stacks.Algebraization.kernel_finiteLength · Stacks.Algebraization.cokernel_finiteLength · Stacks.Algebraization.PreparedExtension.eulerCharacteristic_eq · Stacks.Algebraization.eulerCharacteristic_add_of_shortExact · Stacks.Algebraization.CoherentTriple.eulerCharacteristic_add_of_shortExact · Stacks.Algebraization.exists_polynomial_natDegree_le_dim_supp

Section52.26 Invertible modules on punctured spectra, I #

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

Tag 0F2A, a lemma

Tag 0F2A in the Stacks Project.

Stacks.Algebraization.picRestrictionInjOnTorsion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/PuncturedSpectrumPicardTorsion.lean, line 431. The attribute's comment: “conditional only on the polynomiality of the Euler characteristics of the twists (Tag 0F27), which this development does not prove”.

Stacks Project, Tag 0F2A. Let (A, 𝔪) be a Noetherian local ring and let f ∈ 𝔪 be a nonzerodivisor with depth(A/fA) ≥ 2. Let U be the punctured spectrum of A and U₀ the punctured spectrum of A/fA. Then Pic(U) → Pic(U₀) is injective on torsion.

Two classes of finite order with the same restriction have a difference of finite order restricting to zero, and such a difference is zero by Stacks.Algebraization.eq_zero_of_schemePullbackClass_eq_zero_of_isOfFinAddOrder.

Beyond the tag's own hypotheses this carries one thing: hpoly, which is [Stacks, Tag 0F27] and which this development does not prove. It is a statement about Euler characteristics of twists of coherent triples; it mentions neither the Picard group nor any restriction map, so the conclusion is nowhere assumed. The f-torsion-freeness of 𝒪_U that the rest of this section carries is not assumed here -- it is proved, from f being a nonzerodivisor, by Stacks.Algebraization.isFTorsionFree_unitModule.

public theorem picRestrictionInjOnTorsion (A : Type u) [CommRing A] [IsLocalRing A]
    [IsNoetherianRing A] (f : A) (hfm : f ∈ maximalIdeal A) (hreg : IsRegular f)
    (hb : 2 ≤ Module.depth A (maximalIdeal A) (A ⧸ Ideal.span {f}))
    (hpoly : IsCoherentTripleHilbertPolynomial.{u}) :
    Set.InjOn (Stacks.Picard.schemePullbackClass (puncturedClosedFibreRestriction A f))
      {x : Stacks.Picard.ofScheme (Stacks.Divisors.puncturedSpectrum A).toScheme |
        IsOfFinAddOrder x}

Stacks.Algebraization.puncturedClosedFibreRestriction_injOn_torsion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/PuncturedSpectrumPicardTorsionInjective.lean, line 59.

Stacks Project, Tag 0F2A. Let (A, 𝔪) be a Noetherian local ring and let f ∈ 𝔪 be a nonzerodivisor with depth(A/fA) ≥ 2. Let U be the punctured spectrum of A and U₀ the punctured spectrum of A/fA. Then Pic(U) → Pic(U₀) is injective on torsion.

The map is pullback of invertible modules along the restriction U₀ ⟶ U of the closed immersion Spec(A/fA) ⟶ Spec A. This is Stacks.Algebraization.picRestrictionInjOnTorsion with its polynomiality argument supplied by Stacks.Algebraization.isCoherentTripleHilbertPolynomial.

public theorem puncturedClosedFibreRestriction_injOn_torsion (A : Type u) [CommRing A]
    [IsLocalRing A] [IsNoetherianRing A] (f : A) (hfm : f ∈ maximalIdeal A) (hreg : IsRegular f)
    (hb : 2 ≤ Module.depth A (maximalIdeal A) (A ⧸ Ideal.span {f})) :
    Set.InjOn (Stacks.Picard.schemePullbackClass (puncturedClosedFibreRestriction A f))
      {x : Stacks.Picard.ofScheme (Stacks.Divisors.puncturedSpectrum A).toScheme |
        IsOfFinAddOrder x}

Tag 0F2B, a proposition

Tag 0F2B in the Stacks Project.

Stacks.Algebraization.kollar_picRestrictionInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/PuncturedSpectrumPicardKollar.lean, line 290. The attribute's comment: “the proposition: Pic(U) → Pic(U₀) is injective”.

Stacks Project, Tag 0F2B (Kollár). Let (A, 𝔪) be a Noetherian local ring and f ∈ 𝔪. Assume

A has a dualizing complex,

f is a nonzerodivisor,

depth(A/fA) ≥ 2, and

every prime 𝔭 ∋ f with dim(A/𝔭) = 2 has depth(A_𝔭) ≥ 2.

Let U, resp. U₀, be the punctured spectrum of A, resp. of A/fA. Then Pic(U) → Pic(U₀) is injective. Finally, if (1), (2), (3) hold, A satisfies Serre's condition (S₂) and dim(A) ≥ 4, then (4) holds.

This is the proposition's own conclusion, under the source's four hypotheses and nothing else: Stacks.Algebraization.picRestrictionInjective_kollar, after translating hypothesis (3) into depth(A) ≥ 3 by Stacks.Algebraization.le_depth_quotient_span_singleton_iff and replacing the dualizing complex by the unique shift of it that is normalized (Dualizing.exists_isNormalizedDualizingComplex_shift).

The source's closing sentence — that (1), (2), (3) together with (S₂) and dim(A) ≥ 4 imply (4) — is the other half of the tag, and is Stacks.Serre.LocalizationDepth.two_le_ringDepth_localization_of_isDualizingComplex, which carries the tag's attribute for that assertion. The two attribute strings partition the proposition, so this one claims only the injectivity.

public theorem kollar_picRestrictionInjective (A : Type u) [CommRing A] [IsLocalRing A]
    [IsNoetherianRing A] (f : A) (hfm : f ∈ IsLocalRing.maximalIdeal A) :
    ∀ K : DerivedCategory (ModuleCat.{u} A), Dualizing.IsDualizingComplex K →
      IsSMulRegular A f →
      2 ≤ Module.depth A (IsLocalRing.maximalIdeal A) (A ⧸ Ideal.span {f}) →
      (∀ p : Ideal A, ∀ _ : p.IsPrime, f ∈ p → ringKrullDim (A ⧸ p) = 2 →
        2 ≤ Module.depth (Localization.AtPrime p)
          (IsLocalRing.maximalIdeal (Localization.AtPrime p)) (Localization.AtPrime p)) →
      Function.Injective
        (Stacks.Picard.schemePullbackClass (puncturedClosedFibreRestriction A f))

Stacks.Serre.LocalizationDepth.two_le_ringDepth_localization_of_isDualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Serre/LocalizationDepthCodimension.lean, line 165. The attribute's comment: “the last assertion: (S₂) and dimension at least four give hypothesis (4)”.

The last assertion of [Stacks, Tag 0F2B]. Let A be a Noetherian local ring admitting a dualizing complex, satisfying Serre's condition (S₂) and of dimension at least four. Then the localization of A at a prime whose quotient has dimension two has depth at least two, which is the fourth hypothesis of that source's proposition.

A ring with a dualizing complex is universally catenary, hence catenary, so this is the preceding statement. The source restricts the primes to those containing an element f which it assumes to be a nonzerodivisor with depth(A ⧸ fA) ≥ 2; neither f nor those two hypotheses enter the argument.

theorem two_le_ringDepth_localization_of_isDualizingComplex (A : Type u) [CommRing A]
    [IsNoetherianRing A] [IsLocalRing A] {K : DerivedCategory (ModuleCat.{u} A)}
    (hK : Dualizing.IsDualizingComplex K) (hS₂ : PropertySkRing A 2)
    (hdim : 4 ≤ ringKrullDim A) :
    ∀ p : PrimeSpectrum A, ringKrullDim (A ⧸ p.asIdeal) = 2 →
      2 ≤ ringDepth (Localization.AtPrime p.asIdeal)

Tag 0FIX, a remark

Tag 0FIX in the Stacks Project.

Stacks.Algebraization.picRestrictionInjective_of_regularQuotient_of_depth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/PuncturedSpectrumPicardInjectivityDepthFour.lean, line 205. The attribute's comment: “the SGA2 lemma: for a Noetherian local ring that is a quotient of a regular ring and a nonzerodivisor f of the maximal ideal with depth(A/fA) ≥ 3, the map Pic(U) → Pic(U₀) from the punctured spectrum of A to that of A/fA is injective. The five hypotheses of the source are all demanded. The Euler characteristic of the invertible coherent triple completing a module trivial on U₀ is shown to vanish in this depth, which by [Stacks, Tag 0F28] trivialises the module; the finiteness of H^2 of its sections that this needs is [Stacks, Tag 0BPY]. The source's footnote that hypothesis (a) follows from hypothesis (b) is twoLeDepthLocalization_of_dim_eq_one, and the dualizing complex of a quotient of a regular ring is hasDualizingComplexOfRegularQuotient.”. References: SGA 2 XI (3.16), “more general”.

[SGA2, Exposé XI, Lemma 3.16]. Let (A, 𝔪) be a Noetherian local ring and f ∈ 𝔪. Assume A is a quotient of a regular ring R, that f is a nonzerodivisor, and that (a) depth(A_𝔭) ≥ 2 for every prime 𝔭 with dim(A/𝔭) = 1 and (b) depth(A/fA) ≥ 3. Let U, resp. U₀, be the punctured spectrum of A, resp. A/fA. Then Pic(U) → Pic(U₀) is injective.

theorem picRestrictionInjective_of_regularQuotient_of_depth (A : Type u) [CommRing A]
    [IsNoetherianRing A] [IsLocalRing A] (f : A) (hfm : f ∈ maximalIdeal A) (_R : Type u)
    [CommRing _R] [IsRegularRing _R] (_π : _R →+* A) (_hπ : Function.Surjective _π)
    (hf : IsRegular f)
    (_ha : ∀ p : Ideal A, ∀ _ : p.IsPrime, ringKrullDim (A ⧸ p) = 1 → TwoLeDepthLocalization A p)
    (hb : 3 ≤ Module.depth A (maximalIdeal A) (A ⧸ Ideal.span {f})) :
    PicRestrictionInjective A f

Stacks.Algebraization.hasDualizingComplexOfRegularQuotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/PuncturedSpectrumPicardInjectivitySGA2.lean, line 121. The attribute's comment: “item (1): a Noetherian local ring that is a quotient of a regular ring has a dualizing complex”.

A Noetherian local ring that is a quotient of a regular ring has a dualizing complex.

theorem hasDualizingComplexOfRegularQuotient (A : Type u) [CommRing A] [IsNoetherianRing A]
    [IsLocalRing A] : HasDualizingComplexOfRegularQuotient A

Stacks.Algebraization.twoLeDepthLocalization_of_four_le_depth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/PuncturedSpectrumPicardInjectivitySGA2.lean, line 168. The attribute's comment: “item (2): for a Noetherian local ring with depth(A) ≥ 4, every prime 𝔭 with dim(A/𝔭) = 2 (indeed ≤ 2) has depth(A_𝔭) ≥ 2”.

Let A be a Noetherian local ring. If depth(A) ≥ 4 and 𝔭 is a prime with dim(A/𝔭) ≤ 2 then depth(A_𝔭) ≥ 2.

theorem twoLeDepthLocalization_of_four_le_depth (A : Type u) [CommRing A] [IsNoetherianRing A]
    [IsLocalRing A] (hA : 4 ≤ Module.depth A (IsLocalRing.maximalIdeal A) A) (p : Ideal A)
    [p.IsPrime] (hdim : ringKrullDim (A ⧸ p) ≤ 2) :
    TwoLeDepthLocalization A p

Stacks.Algebraization.three_le_depth_quotient_iff_four_le_depth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/PuncturedSpectrumPicardInjectivitySGA2.lean, line 205. The attribute's comment: “hypothesis (b): for f ∈ 𝔪 a nonzerodivisor of a Noetherian local ring, depth(A/fA) ≥ 3 is equivalent to depth(A) ≥ 4”.

Let (A, 𝔪) be a Noetherian local ring and f ∈ 𝔪 a nonzerodivisor. Then depth(A/fA) ≥ 3 if and only if depth(A) ≥ 4.

theorem three_le_depth_quotient_iff_four_le_depth (A : Type u) [CommRing A]
    [IsNoetherianRing A] [IsLocalRing A] (f : A) (hfm : f ∈ IsLocalRing.maximalIdeal A)
    (hf : IsSMulRegular A f) :
    3 ≤ Module.depth A (IsLocalRing.maximalIdeal A) (A ⧸ Ideal.span {f}) ↔
      4 ≤ Module.depth A (IsLocalRing.maximalIdeal A) A

Stacks.Algebraization.twoLeDepthLocalization_of_dim_eq_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/PuncturedSpectrumPicardInjectivitySGA2.lean, line 224. The attribute's comment: “footnote: (b) implies (a) -- for f ∈ 𝔪 a nonzerodivisor of a Noetherian local ring with depth(A/fA) ≥ 3, every prime 𝔭 with dim(A/𝔭) = 1 has depth(A_𝔭) ≥ 2”.

Let (A, 𝔪) be a Noetherian local ring. If f ∈ 𝔪 is a nonzerodivisor with depth(A/fA) ≥ 3, then every prime 𝔭 with dim(A/𝔭) = 1 has depth(A_𝔭) ≥ 2.

theorem twoLeDepthLocalization_of_dim_eq_one (A : Type u) [CommRing A] [IsNoetherianRing A]
    [IsLocalRing A] (f : A) (hfm : f ∈ IsLocalRing.maximalIdeal A) (hf : IsSMulRegular A f)
    (hb : 3 ≤ Module.depth A (IsLocalRing.maximalIdeal A) (A ⧸ Ideal.span {f})) (p : Ideal A)
    [p.IsPrime] (hdim : ringKrullDim (A ⧸ p) = 1) :
    TwoLeDepthLocalization A p

Stacks.Algebraization.kollarHypotheses_of_regularQuotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/PuncturedSpectrumPicardInjectivitySGA2.lean, line 244. The attribute's comment: “the deduction from 0F2B: the hypotheses of the SGA2 lemma (a Noetherian local ring that is a quotient of a regular ring, f ∈ 𝔪 a nonzerodivisor, depth(A/fA) ≥ 3) give the four hypotheses of 0F2B -- a dualizing complex by item (1), f a nonzerodivisor, depth(A/fA) ≥ 2, and depth(A_𝔭) ≥ 2 for every prime 𝔭 ∋ f with dim(A/𝔭) = 2 by item (2)”.

The hypotheses of the SGA2 lemma give the four hypotheses of Kollár's proposition [Stacks, Tag 0F2B]. Let (A, 𝔪) be a Noetherian local ring, f ∈ 𝔪, and assume A is a quotient of a regular ring R, that f is a nonzerodivisor and that depth(A/fA) ≥ 3. Then

A has a dualizing complex,

f is a nonzerodivisor,

depth(A/fA) ≥ 2, and

every prime 𝔭 ∋ f with dim(A/𝔭) = 2 has depth(A_𝔭) ≥ 2.

theorem kollarHypotheses_of_regularQuotient (A : Type u) [CommRing A] [IsNoetherianRing A]
    [IsLocalRing A] (f : A) (hfm : f ∈ IsLocalRing.maximalIdeal A) (R : Type u) [CommRing R]
    [IsRegularRing R] (π : R →+* A) (hπ : Function.Surjective π) (hf : IsSMulRegular A f)
    (hb : 3 ≤ Module.depth A (IsLocalRing.maximalIdeal A) (A ⧸ Ideal.span {f})) :
    (∃ K : DerivedCategory (ModuleCat.{u} A), Dualizing.IsDualizingComplex K) ∧
      IsSMulRegular A f ∧
      2 ≤ Module.depth A (IsLocalRing.maximalIdeal A) (A ⧸ Ideal.span {f}) ∧
      ∀ p : Ideal A, ∀ _ : p.IsPrime, f ∈ p → ringKrullDim (A ⧸ p) = 2 →
        TwoLeDepthLocalization A p

Sources

LeanStacks.Algebraization.picRestrictionInjOnTorsion · Stacks.Algebraization.puncturedClosedFibreRestriction_injOn_torsion · Stacks.Algebraization.kollar_picRestrictionInjective · Stacks.Serre.LocalizationDepth.two_le_ringDepth_localization_of_isDualizingComplex · Stacks.Algebraization.picRestrictionInjective_of_regularQuotient_of_depth · Stacks.Algebraization.hasDualizingComplexOfRegularQuotient · Stacks.Algebraization.twoLeDepthLocalization_of_four_le_depth · Stacks.Algebraization.three_le_depth_quotient_iff_four_le_depth

Section52.27 Invertible modules on punctured spectra, II #

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

Tag 0F2D, a lemma

Tag 0F2D in the Stacks Project.

Stacks.PuncturedSpectrumPicard.picardColimitSurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PuncturedSpectrumPicard/FormalPicardAlgebraization.lean, line 373.

[Stacks, Tag 0F2D]. Let (A, 𝔪) be a Noetherian local ring and f ∈ 𝔪. Assume

A is f-adically complete,

f is a nonzerodivisor,

H¹_𝔪(A/fA) and H²_𝔪(A/fA) are finite A-modules, and

H³_𝔪(A/fA) = 0.

Let U, resp. U₀, be the punctured spectrum of A, resp. of A/fA. Then colim_{U₀ ⊆ U' ⊆ U open} Pic(U') ⟶ Pic(U₀) is surjective: every invertible module on U₀ is the restriction of an invertible module on an open U' of U containing U₀. The conclusion is Stacks.PuncturedSpectrumPicard.PicardColimitSurjective, the elementwise form of surjectivity out of the filtered colimit.

The proof is the source's. A class on U₀ extends to a compatible family along the infinitesimal neighbourhoods Uₙ = V((f𝒪_U)ⁿ⁺¹) by [Stacks, Tag 0C6R] and H²(U₀, 𝒪_{U₀}) = H³_𝔪(A/fA) = 0 (exists_compatible_idealPowerStages); the representing invertible modules, pushed forward to U, form a finite locally free object of Coh(U, f𝒪_U) (Stacks.Coherent.IdealPowerStageModules); by [Stacks, Tag 0EKZ] it is the completion of a finite locally free 𝒢 on an open V ⊇ U₀ (exists_completion_iso_of_eq_situation); 𝒢 restricts to the given module on U₀ (Stacks.Coherent.IdealPowerStageModules.exists_pullback_iso_of_completion_iso) and is therefore invertible on an open U' ⊇ U₀ (exists_opens_isInvertible_of_pullback_iso).

theorem picardColimitSurjective [IsNoetherianRing A] (hf : f ∈ maximalIdeal A)
    (hcomplete : IsAdicComplete (Ideal.span {f}) A) (hreg : IsSMulRegular A f)
    (hH1 : Module.Finite A (Stacks.LocalCohomology.localCohomologyWithSupportIn.{u, u} A
      {closedPoint A} ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
        (ModuleCat.of A (A ⧸ Ideal.span {f}))) 1))
    (hH2 : Module.Finite A (Stacks.LocalCohomology.localCohomologyWithSupportIn.{u, u} A
      {closedPoint A} ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
        (ModuleCat.of A (A ⧸ Ideal.span {f}))) 2))
    (hvanish3 : IsZero (Stacks.LocalCohomology.localCohomologyWithSupportIn.{u, u} A
      {closedPoint A} ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
        (ModuleCat.of A (A ⧸ Ideal.span {f}))) 3)) :
    PicardColimitSurjective A f

Stacks.PuncturedSpectrumPicard.exists_isCompatible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PuncturedSpectrumPicard/FormalTower.lean, line 190. The attribute's comment: “the first half of the source's proof, in the generality the argument has: for a tower of first-order thickenings whose ideal sheaves have vanishing H², every Picard class on the bottom stage extends to a compatible family along the whole tower. That is the source's step Pic(U_{n+1}) → Pic(U_n) → H²(U₀,𝒪_{U₀}) = H³_𝔪(A/fA) = 0, therefore each invertible 𝒪_{U₀}-module is restricted from an invertible object of Coh(U,f𝒪_U), and the single-stage lift is Stacks 0C6R, Stacks.Thickenings.exact_picardRestriction in StacksFrontier.AlgebraicGeometry.Thickenings.PicardSequence. The vanishing of H² is a condition on the tower, not every tower satisfying it; for the same half at the punctured spectrum, with that vanishing derived from the source's own hypotheses (2) f a nonzerodivisor and (4) H³_𝔪(A/fA) = 0, see Stacks.PuncturedSpectrumPicard.exists_isCompatiblePullback_puncturedSpectrum. NOT covered by this declaration: the tag's own conclusion, surjectivity of colim_{U₀ ⊆ U' ⊆ U} Pic(U') → Pic(U₀), written as Stacks.PuncturedSpectrumPicard.PicardColimitSurjective, which needs Stacks 0EKZ and through it Stacks 0EIR part (2)”.

The first half of the proof of [Stacks, Tag 0F2D]. Let X₀ ⟶ X₁ ⟶ X₂ ⟶ ⋯ be a tower of first-order thickenings in which the ideal sheaf of every stage has vanishing second cohomology. Then every Picard class on the bottom stage extends to a compatible family of Picard classes along the whole tower.

This is the step the source writes as "this gives an exact sequence Pic(U_{n+1}) → Pic(U_n) → H²(U₀, 𝒪_{U₀}) = H³_𝔪(A/fA) = 0. Therefore each invertible 𝒪_{U₀}-module is restricted from an invertible object of Coh(U, f𝒪_U)." Each single lift is surjective_picardRestriction_of_forall_eq_zero, and the family is assembled by recursion on the stage, choosing a lift at each step.

What remains of the tag after this is [Stacks, Tag 0EKZ], which descends the formal object so obtained to an invertible module on an open U' with U₀ ⊆ U' ⊆ U; see Stacks.PuncturedSpectrumPicard.PicardColimitSurjective for the conclusion that needs it.

theorem exists_isCompatible
    (h2 : ∀ n, ∀ x : CategoryTheory.Sheaf.H.{u}
      (Stacks.Thickenings.idealAddSheafOnSub (T.hom n)) 2, x = 0)
    (c₀ : Pic (T.obj 0)) :
    ∃ c : (n : ℕ) → Pic (T.obj n), c 0 = c₀ ∧ IsCompatible T c

Stacks.PuncturedSpectrumPicard.exists_isCompatiblePullback_puncturedSpectrum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PuncturedSpectrumPicard/PuncturedSpectrumFirstHalf.lean, line 212. The attribute's comment: “the first half of the source's proof at the punctured spectrum itself, under the source's own hypotheses (2) f a nonzerodivisor and (4) H³_𝔪(A/fA) = 0 and nothing else: every Picard class on U₀ extends to a family along the tower of infinitesimal neighbourhoods of U₀ in U, each the pullback of the next. The per-stage vanishing H²(U_n's ideal sheaf) = 0 is proved here, not assumed: the layers are identified with 𝒪_{U₀} by multiplication by f^{n+1} (Stacks.Thickenings.idealSheafIsoStructureSheafNthOrderBottom, which is where (2) enters) and H²(U₀,𝒪_{U₀}) = 0 is derived from (4). NOT covered: the tag's own conclusion, surjectivity of colim_{U₀ ⊆ U' ⊆ U} Pic(U') → Pic(U₀), which is the second half and needs Stacks 0EKZ, hence Stacks 0EIR part (2); hypotheses (1) f-adic completeness and (3) finiteness of H¹_𝔪(A/fA), H²_𝔪(A/fA) are inputs of that half alone and do not appear here”.

The first half of the proof of [Stacks, Tag 0F2D]. Let (A, 𝔪) be a Noetherian local ring and let f ∈ 𝔪 be a nonzerodivisor with H³_𝔪(A/fA) = 0. Then every Picard class on the bottom stage of the tower of infinitesimal neighbourhoods of U₀ in the punctured spectrum U extends to a family of classes along the whole tower, each the pullback of the next.

Only hypotheses (2) and (4) of the tag are used. The tower is Stacks.PuncturedSpectrumPicard.infinitesimalTower of Stacks.PuncturedSpectrumPicard.puncturedPrincipalImmersion, the layers are all 𝒪_{U₀} because f is a nonzerodivisor generating the ideal sheaf on every chart, and the single-stage lift is the exact sequence of [Stacks, Tag 0C6R].

theorem exists_isCompatiblePullback_puncturedSpectrum [IsNoetherianRing A]
    (hf : f ∈ maximalIdeal A) (hreg : IsSMulRegular A f)
    (hvanish3 : IsZero (Stacks.LocalCohomology.localCohomologyWithSupportIn.{u, u} A
      {closedPoint A} ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
        (ModuleCat.of A (A ⧸ Ideal.span {f}))) 3))
    (c₀ : Stacks.Picard.ofScheme
      (nthOrderInfinitesimalNeighbourhood (puncturedPrincipalImmersion A f) 0)) :
    ∃ c : (n : ℕ) → Stacks.Picard.ofScheme
        ((infinitesimalTower (puncturedPrincipalImmersion A f)).obj n),
      c 0 = c₀ ∧
        IsCompatiblePullback (infinitesimalTower (puncturedPrincipalImmersion A f)) c

Tag 0F2E, a remark

Tag 0F2E in the Stacks Project.

Stacks.PuncturedSpectrumPicard.picardColimitSurjective_of_isDualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PuncturedSpectrumPicard/DualizingPicardAlgebraization.lean, line 85. The attribute's comment: “the whole remark: under (1)-(5) the conclusion of 0F2D holds; points (a) and (b) are commentary with no mathematical claim”.

[Stacks, Tag 0F2E]. Let (A, 𝔪) be a Noetherian local ring and f ∈ 𝔪. Assume

A has a dualizing complex,

A is f-adically complete,

f is a nonzerodivisor,

one of the following is true

(a) A_f is (S₂) and for 𝔭 ⊂ A, f ∉ 𝔭 minimal we have dim(A/𝔭) ≥ 4, or

(b) if 𝔭 ∉ V(f) and V(𝔭) ∩ V(f) ≠ {𝔪}, then depth(A_𝔭) + dim(A/𝔭) > 3,

H³_𝔪(A/fA) = 0.

Then the conclusion of [Stacks, Tag 0F2D] holds: with U, resp. U₀, the punctured spectrum of A, resp. of A/fA, the map colim_{U₀ ⊆ U' ⊆ U open} Pic(U') ⟶ Pic(U₀) is surjective. As for [Stacks, Tag 0F2D] (Stacks.PuncturedSpectrumPicard.picardColimitSurjective), the conclusion is Stacks.PuncturedSpectrumPicard.PicardColimitSurjective, the elementwise form of surjectivity out of the filtered colimit: every invertible module on U₀ is the restriction of an invertible module on an open U' of U containing U₀.

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. Hypothesis (1) is read in any model [HasDerivedCategory (ModuleCat A)] of the derived category; whether a dualizing complex exists does not depend on the model. These are the spellings of [Stacks, Tag 0EKY] (Stacks.Algebraization.completionEquivalence_local_principal_finiteLocallyFree). Hypothesis (5) is written, as in [Stacks, Tag 0F2D], in the library's default model, before the model of (1) is introduced, so that the two do not interfere.

The proof is the source's: that of [Stacks, Tag 0F2D] with [Stacks, Tag 0EKY] in place of [Stacks, Tag 0EKZ]. A class on U₀ extends along the infinitesimal neighbourhoods of U₀ by [Stacks, Tag 0C6R] and H²(U₀, 𝒪_{U₀}) = H³_𝔪(A/fA) = 0, giving an invertible object of Coh(U, f𝒪_U); by the essential surjectivity of [Stacks, Tag 0EKY] it is the completion of a finite locally free module on an open V ⊇ U₀, which is invertible near U₀ (Stacks.PuncturedSpectrumPicard.picardColimitSurjective_of_forall_isCompletionNearClosed).

theorem picardColimitSurjective_of_isDualizingComplex [IsNoetherianRing A]
    (hf : f ∈ maximalIdeal A)
    (hcomplete : IsAdicComplete (Ideal.span {f}) A) (hreg : IsSMulRegular A f)
    (hvanish3 : IsZero (Stacks.LocalCohomology.localCohomologyWithSupportIn.{u, u} A
      {closedPoint A} ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
        (ModuleCat.of A (A ⧸ Ideal.span {f}))) 3))
    [HasDerivedCategory.{w} (ModuleCat.{u} A)]
    (hdual : ∃ K : DerivedCategory (ModuleCat.{u} A), Dualizing.IsDualizingComplex K)
    (hcond :
      (PropertySkRing (Localization.Away f) 2 ∧
        ∀ p : PrimeSpectrum A, IsMinimalPrime p.asIdeal → f ∉ p.asIdeal →
          (4 : WithBot ℕ∞) ≤ ringKrullDim (A ⧸ p.asIdeal)) ∨
      (∀ p : PrimeSpectrum A, f ∉ p.asIdeal →
        ({q : PrimeSpectrum A | p.asIdeal ≤ q.asIdeal} ∩
          {q : PrimeSpectrum A | f ∈ q.asIdeal}) ≠
          {⟨maximalIdeal A, (maximalIdeal.isMaximal A).isPrime⟩} →
        (3 : WithBot ℕ∞) <
          (Module.depth (Localization.AtPrime p.asIdeal)
            (maximalIdeal (Localization.AtPrime p.asIdeal))
            (Localization.AtPrime p.asIdeal) : WithBot ℕ∞) +
            ringKrullDim (A ⧸ p.asIdeal))) :
    PicardColimitSurjective A f

Tag 0F2F, a lemma

Tag 0F2F in the Stacks Project.

Stacks.PuncturedSpectrumPicard.surjective_schemePullbackClass_puncturedClosedFibre_of_isNoetherianRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PuncturedSpectrumPicard/ExtensionAcrossPoint.lean, line 533. The attribute's comment: “GRANTED, and not proved here, ONE input: h0F2D, the conclusion of Stacks 0F2D for (A,f), carried as Stacks.PuncturedSpectrumPicard.PicardColimitSurjective — the predicate the restricted 0F2D of StacksFrontier.AlgebraicGeometry.PuncturedSpectrumPicard.FormalTower states unproved and explicitly disclaims, so that tag's restriction is inherited here. The source's other input, By Limits, Lemma 0F21 applied n times, is NO LONGER granted: the one-point step is proved as Stacks.PuncturedSpectrumPicard.picardExtendsAcrossPoint and supplied here. Clause (2) of the source is h2, transcribed with the two standard identifications performed in the statement: a maximal ideal of A_f is a prime 𝔭 of A with f ∉ 𝔭 maximal among such, and (A_f)_𝔭 = A_𝔭 = Localization.AtPrime 𝔭”.

Stacks 0F2F, with the one-point extension step discharged. Surjectivity of Pic(U) ⟶ Pic(U₀) for the punctured spectrum U of a Noetherian local ring A and the punctured spectrum U₀ of A/fA.

This is Stacks.PuncturedSpectrumPicard.surjective_schemePullbackClass_puncturedClosedFibre with its hstep hypothesis supplied by picardExtendsAcrossPoint, so the only input still granted is the conclusion of [Stacks, Tag 0F2D].

theorem surjective_schemePullbackClass_puncturedClosedFibre_of_isNoetherianRing
    (hf : f ∈ maximalIdeal A) (h0F2D : PicardColimitSurjective A f)
    (h2 : ∀ p : PrimeSpectrum A, f ∉ p.asIdeal →
      (∀ q : PrimeSpectrum A, p.asIdeal < q.asIdeal → f ∈ q.asIdeal) →
      Subsingleton (Stacks.Picard.ofScheme
        (Stacks.Divisors.puncturedSpectrum (Localization.AtPrime p.asIdeal)).toScheme)) :
    Function.Surjective (Stacks.Picard.schemePullbackClass
      (morphismRestrict (Stacks.Algebraization.closedImmersion A f)
        (Stacks.Divisors.puncturedSpectrum A)))

Stacks.PuncturedSpectrumPicard.surjective_schemePullbackClass_puncturedClosedFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PuncturedSpectrumPicard/ExtensionToPuncturedSpectrum.lean, line 527. The attribute's comment: “GRANTED, and NOT proved anywhere in this file, two inputs, both carried as hypotheses: (i) h0F2D, the conclusion of Stacks 0F2D for (A,f), which is clause (1) the conditions of Lemma 0F2D hold of the source read through that lemma's conclusion — it is Stacks.PuncturedSpectrumPicard.PicardColimitSurjective, the predicate the restricted 0F2D of StacksFrontier.AlgebraicGeometry.PuncturedSpectrumPicard.FormalTower states unproved and explicitly disclaims, so the restriction of that tag is inherited here; and (ii) hstep, Stacks.PuncturedSpectrumPicard.PicardExtendsAcrossPoint, the extension of an invertible module across ONE point 𝔭 of ONE open of Spec A whose local ring has punctured spectrum with trivial Picard group — the source's By Limits, Lemma 0F21 applied n times for a single n, which needs the Pic-versus-FinitePresentationModules translation and the identification of 𝒪_{Spec A,𝔭} with A_𝔭 before Stacks 0F21 (proved here as AlgebraicGeometry.GlueingNearPoint.moduleGlueingEquivalenceNearClosedPoint) can discharge it. PROVED here, from those two: everything else in the source's proof — that U ∖ U' lies in D(f), is FINITE, and consists of points closed in U and maximal in A_f (the source's points corresponding to prime ideals 𝔭₁,…,𝔭ₙ as in (2)), and the induction applying the one-point step n times. Clause (2) of the source is hypothesis h2, transcribed with the two standard identifications performed in the statement: a maximal ideal of A_f is a prime 𝔭 of A with f ∉ 𝔭 maximal among such, and (A_f)_𝔭 = A_𝔭 = Localization.AtPrime 𝔭”.

[Stacks, Tag 0F2F]. Let (A, 𝔪) be a Noetherian local ring and f ∈ 𝔪. Write U for the punctured spectrum of A and U₀ for the punctured closed fibre. Granted the conclusion of [Stacks, Tag 0F2D] for (A, f) and the one-point extension step PicardExtendsAcrossPoint, and assuming that every maximal ideal 𝔭 of A_f has Pic of the punctured spectrum of A_𝔭 trivial, restriction Pic(U) → Pic(U₀) is surjective.

A class on U₀ comes, by [Stacks, Tag 0F2D], from a class on some open U₀ ⊆ U' ⊆ U. The exceptional set U ∖ U' is finite and consists of points closed in U and maximal in A_f (finite_exceptionalPoints, isOpen_puncturedSpectrum_sdiff_singleton, eq_closedPoint_of_lt_of_mem_exceptionalPoints), so the class extends across those points one at a time by surjective_schemePullbackClass_homOfLE_of_finite.

theorem surjective_schemePullbackClass_puncturedClosedFibre (hf : f ∈ maximalIdeal A)
    (hstep : PicardExtendsAcrossPoint A) (h0F2D : PicardColimitSurjective A f)
    (h2 : ∀ p : PrimeSpectrum A, f ∉ p.asIdeal →
      (∀ q : PrimeSpectrum A, p.asIdeal < q.asIdeal → f ∈ q.asIdeal) →
      Subsingleton (Stacks.Picard.ofScheme
        (Stacks.Divisors.puncturedSpectrum (Localization.AtPrime p.asIdeal)).toScheme)) :
    Function.Surjective (Stacks.Picard.schemePullbackClass
      (morphismRestrict (Stacks.Algebraization.closedImmersion A f)
        (Stacks.Divisors.puncturedSpectrum A)))

Stacks.PuncturedSpectrumPicard.surjective_schemePullbackClass_puncturedClosedFibre_of_localCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PuncturedSpectrumPicard/PicardSurjectivePuncturedSpectrum.lean, line 123. The attribute's comment: “the full statement: under the four conditions of Stacks 0F2D (f-adic completeness, f a nonzerodivisor, finiteness of H^1_m(A/fA) and H^2_m(A/fA), vanishing of H^3_m(A/fA)) and triviality of Pic of the punctured spectrum of (A_f)_P for every maximal ideal P of A_f, restriction Pic(U) -> Pic(U_0) is surjective”.

[Stacks, Tag 0F2F]. Let (A, 𝔪) be a Noetherian local ring and f ∈ 𝔪. Assume (1) the conditions of [Stacks, Tag 0F2D]: A is f-adically complete, f is a nonzerodivisor, H¹_𝔪(A/fA) and H²_𝔪(A/fA) are finite A-modules and H³_𝔪(A/fA) = 0; and (2) for every maximal ideal 𝔓 of A_f the punctured spectrum of (A_f)_𝔓 has trivial Picard group. Let U, resp. U₀, be the punctured spectrum of A, resp. A/fA. Then Pic(U) → Pic(U₀) is surjective.

A class on U₀ comes from a class on an open U₀ ⊆ U' ⊆ U by [Stacks, Tag 0F2D] (picardColimitSurjective); the complement U ∖ U' is a finite set of points that are maximal ideals of A_f, and the class extends across each of them by [Stacks, Tag 0F21] (surjective_schemePullbackClass_puncturedClosedFibre_of_isNoetherianRing), hypothesis (2) being read at those points by subsingleton_picard_localizationAtPrime_of_away.

U₀ is Stacks.Algebraization.puncturedClosedFibre A f, the part of Spec(A/fA) over U, which is the punctured spectrum of A/fA (Stacks.PuncturedSpectrumPicard.puncturedClosedFibre_eq_puncturedSpectrum_quotient).

theorem surjective_schemePullbackClass_puncturedClosedFibre_of_localCohomology
    [IsLocalRing A] [IsNoetherianRing A] (hf : f ∈ maximalIdeal A)
    (hcomplete : IsAdicComplete (Ideal.span {f}) A) (hreg : IsSMulRegular A f)
    (hH1 : Module.Finite A (Stacks.LocalCohomology.localCohomologyWithSupportIn.{u, u} A
      {closedPoint A} ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
        (ModuleCat.of A (A ⧸ Ideal.span {f}))) 1))
    (hH2 : Module.Finite A (Stacks.LocalCohomology.localCohomologyWithSupportIn.{u, u} A
      {closedPoint A} ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
        (ModuleCat.of A (A ⧸ Ideal.span {f}))) 2))
    (hvanish3 : IsZero (Stacks.LocalCohomology.localCohomologyWithSupportIn.{u, u} A
      {closedPoint A} ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj
        (ModuleCat.of A (A ⧸ Ideal.span {f}))) 3))
    (h2 : ∀ (P : Ideal (Localization.Away f)) [P.IsMaximal],
      Subsingleton (Stacks.Picard.ofScheme
        (Stacks.Divisors.puncturedSpectrum (Localization.AtPrime P)).toScheme)) :
    Function.Surjective (Stacks.Picard.schemePullbackClass
      (morphismRestrict (Stacks.Algebraization.closedImmersion A f)
        (Stacks.Divisors.puncturedSpectrum A)))

Tag 0F2G, a lemma

Tag 0F2G in the Stacks Project.

Stacks.AlgebraicGeometry.PicardBaseChange.injective_schemePullbackClass_puncturedSpectrumCompletionMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardBaseChange/PuncturedSpectrumCompletion.lean, line 393.

Stacks Project, Tag 0F2G. Let (A, 𝔪) be a Noetherian local ring of depth at least two, let A^ be its completion and let U, resp. U^, be the punctured spectrum of A, resp. A^. Then Pic(U) ⟶ Pic(U^) is injective.

theorem injective_schemePullbackClass_puncturedSpectrumCompletionMap
    (hdepth : 2 ≤ Module.depth A (maximalIdeal A) A) :
    Function.Injective
      (Stacks.Picard.schemePullbackClass (puncturedSpectrumCompletionMap A))

Tag 0F2H, a lemma

Tag 0F2H in the Stacks Project.

Stacks.PicardUFD.subsingleton_picardGroup_puncturedSpectrum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PicardGroup/PuncturedSpectrumRegular.lean, line 57. References: SGA 2 XI (3.13), “XI.3.13(i)”.

Stacks Project, Tag 0F2H. Let (A, 𝔪) be a regular local ring. Then the Picard group of the punctured spectrum Spec A ∖ {𝔪} of A is trivial.

theorem subsingleton_picardGroup_puncturedSpectrum (A : Type u) [CommRing A]
    [IsRegularLocalRing A] :
    Subsingleton (Stacks.Divisors.puncturedSpectrum A).toScheme.picardGroup

Tag 0F2I, a proposition

Tag 0F2I in the Stacks Project.

Stacks.PuncturedSpectrumPicard.subsingleton_picardGroup_puncturedSpectrum_of_isCompleteIntersectionRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PuncturedSpectrumPicard/CompleteIntersection.lean, line 687. The attribute's comment: “GRANTED, not proved here: h0F2D, the conclusion of Stacks 0F2D as PicardColimitSurjective, under that tag's conditions (1), (2) and its footnote's depth bound”.

[Stacks, Tag 0F2I]. Let (A, 𝔪) be a Noetherian local ring. If A is a complete intersection of dimension at least four, then the Picard group of the punctured spectrum U = Spec A ∖ {𝔪} of A is trivial.

Granted, and not proved anywhere in this library, is the conclusion of [Stacks, Tag 0F2D]: it is carried as the hypothesis h0F2D, phrased with the library's own Stacks.PuncturedSpectrumPicard.PicardColimitSurjective and quantified over the Noetherian local rings B that are 𝔪-adically complete, the elements g ∈ 𝔪_B that are nonzerodivisors, and the bound 5 ≤ depth(B). Completeness and the nonzerodivisor clause are conditions (1) and (2) of the source's [Stacks, Tag 0F2D], and the depth bound is that tag's own footnote, "(3) and (4) hold if depth(A/fA) ≥ 4, or equivalently depth(A) ≥ 5", which covers its remaining conditions (3) and (4). So h0F2D asserts no more than [Stacks, Tag 0F2D] does, and a proof of that tag discharges it.

The induction applies it exactly to the intermediate quotients A' = B/(f₁, …, f_{r-1}) of the source's presentation: all are complete because the presenting ring is, and all have depth(A') = dim(A') = dim(A) + 1 ≥ 5 because a quotient of a regular local ring by a regular sequence is Cohen-Macaulay.

theorem subsingleton_picardGroup_puncturedSpectrum_of_isCompleteIntersectionRing
    (A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    (h0F2D : ∀ (B : Type u) [CommRing B] [IsNoetherianRing B] [IsLocalRing B]
      [IsAdicComplete (maximalIdeal B) B] (g : B), g ∈ maximalIdeal B →
      g ∈ nonZeroDivisors B → 5 ≤ Module.depth B (maximalIdeal B) B →
      PicardColimitSurjective B g)
    (hA : LocalCompleteIntersection.IsCompleteIntersectionRing A)
    (hdim : 4 ≤ ringKrullDim A) :
    Subsingleton (Stacks.Divisors.puncturedSpectrum A).toScheme.picardGroup

Stacks.PuncturedSpectrumPicard.subsingleton_picardGroup_puncturedSpectrum_of_completeIntersection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PuncturedSpectrumPicard/CompleteIntersectionPicardTrivial.lean, line 115. References: SGA 2 XI (3.13), “XI.3.13(ii)”; SGA 2 XII (4.9), “4.9 b)”.

Let (A, 𝔪) be a Noetherian local ring. If A is a complete intersection of dimension at least four, then the Picard group of the punctured spectrum U = Spec A ∖ {𝔪} of A is trivial.

theorem subsingleton_picardGroup_puncturedSpectrum_of_completeIntersection
    (A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    (hA : LocalCompleteIntersection.IsCompleteIntersectionRing A)
    (hdim : 4 ≤ ringKrullDim A) :
    Subsingleton (Stacks.Divisors.puncturedSpectrum A).toScheme.picardGroup

Tag 0F2J, an example

Tag 0F2J in the Stacks Project.

Stacks.PuncturedSpectrumPicard.QuadricCone.hypersurface, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PuncturedSpectrumPicard/QuadricConeExample.lean, line 120. The attribute's comment: “the hypersurface”.

The complete local hypersurface cut out by the determinant equation.

public abbrev hypersurface (k : Type u) [Field k]

Stacks.PuncturedSpectrumPicard.QuadricCone.coordinateIdeal, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PuncturedSpectrumPicard/QuadricConeExample.lean, line 129. The attribute's comment: “the ideal (x,z)”.

The ideal generated by the first and third coordinates.

public abbrev coordinateIdeal (k : Type u) [Field k] : Ideal (hypersurface k)

Stacks.PuncturedSpectrumPicard.QuadricCone.hypersurface_isLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PuncturedSpectrumPicard/QuadricConeExample.lean, line 217. The attribute's comment: “local ring”.

The ring k⟦x,y,z,w⟧/(xy - zw) is a local ring.

public theorem hypersurface_isLocalRing (k : Type u) [Field k] :
    IsLocalRing (hypersurface k)

Stacks.PuncturedSpectrumPicard.QuadricCone.hypersurface_isNoetherianRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PuncturedSpectrumPicard/QuadricConeExample.lean, line 225. The attribute's comment: “Noetherian ring”.

The ring k⟦x,y,z,w⟧/(xy - zw) is Noetherian.

public theorem hypersurface_isNoetherianRing (k : Type u) [Field k] :
    IsNoetherianRing (hypersurface k)

Stacks.PuncturedSpectrumPicard.QuadricCone.hypersurface_isCompleteIntersectionRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PuncturedSpectrumPicard/QuadricConeExample.lean, line 366. The attribute's comment: “complete intersection”.

The ring k⟦x,y,z,w⟧/(xy - zw) is a complete intersection ring.

public theorem hypersurface_isCompleteIntersectionRing (k : Type u) [Field k] :
    LocalCompleteIntersection.IsCompleteIntersectionRing (hypersurface k)

Stacks.PuncturedSpectrumPicard.QuadricCone.hypersurface_krullDim, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PuncturedSpectrumPicard/QuadricConeExample.lean, line 421. The attribute's comment: “dimension three”.

The ring k⟦x,y,z,w⟧/(xy - zw) has Krull dimension three.

public theorem hypersurface_krullDim (k : Type u) [Field k] :
    ringKrullDim (hypersurface k) = 3

Stacks.PuncturedSpectrumPicard.QuadricCone.coordinateIdeal_not_principal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PuncturedSpectrumPicard/QuadricConeExample.lean, line 537. The attribute's comment: “nonprincipal ideal”.

The ideal (x,z) of k⟦x,y,z,w⟧/(xy - zw) is not generated by a single element.

public theorem coordinateIdeal_not_principal (k : Type u) [Field k] :
    ¬ ∃ a : hypersurface k, coordinateIdeal k = Ideal.span ({a} : Set (hypersurface k))

Stacks.PuncturedSpectrumPicard.QuadricCone.quotient_depth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PuncturedSpectrumPicard/QuadricConeExample.lean, line 581. The attribute's comment: “quotient depth”.

The quotient of A = k⟦x,y,z,w⟧/(xy - zw) by the ideal (x,z) has depth two as an A-module, along the maximal ideal of A.

public theorem quotient_depth (k : Type u) [Field k] :
    Module.depth (hypersurface k) (IsLocalRing.maximalIdeal (hypersurface k))
      (hypersurface k ⧸ coordinateIdeal k) = 2

Stacks.PuncturedSpectrumPicard.QuadricCone.coordinateIdeal_depth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PuncturedSpectrumPicard/QuadricConeExample.lean, line 637. The attribute's comment: “ideal depth”.

The ideal (x,z) of A = k⟦x,y,z,w⟧/(xy - zw) has depth three as an A-module, along the maximal ideal of A.

public theorem coordinateIdeal_depth (k : Type u) [Field k] :
    Module.depth (hypersurface k) (IsLocalRing.maximalIdeal (hypersurface k))
      (coordinateIdeal k) = 3

Stacks.PuncturedSpectrumPicard.QuadricCone.negativeTwist_not_trivial', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PuncturedSpectrumPicard/QuadricConeExample.lean, line 1164. The attribute's comment: “nontrivial line bundle”.

The sheaf 𝒪_U(-D) = ℐ_D on the punctured spectrum U of A = k⟦x,y,z,w⟧/(xy - zw), for the divisor D cut out by I = (x,z), is not a trivial invertible 𝒪_U-module.

public theorem negativeTwist_not_trivial' (k : Type u) [Field k] :
    ¬ Stacks.SheafOfModules.IsTrivial
        (Stacks.Divisors.puncturedSpectrum (hypersurface k)).toScheme.presheaf
        (Stacks.Divisors.puncturedSpectrum (hypersurface k)).toScheme.ringCatIsSheaf
        (Stacks.Divisors.negativeTwist' (cartierDivisor k))

Stacks.PuncturedSpectrumPicard.QuadricCone.picardGroup_not_subsingleton', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PuncturedSpectrumPicard/QuadricConeExample.lean, line 1205. The attribute's comment: “the conclusion: Pic(U) is nontrivial, at the same Scheme.picardGroup that Stacks 0F2I is stated at, so this is literally the negation of that proposition's conclusion for this A”.

The Picard group AlgebraicGeometry.Scheme.picardGroup of the punctured spectrum U = Spec A ∖ {𝔪} of A = k⟦x,y,z,w⟧/(xy - zw) is nontrivial.

public theorem picardGroup_not_subsingleton' (k : Type u) [Field k] :
    ¬ Subsingleton
      (Stacks.Divisors.puncturedSpectrum (hypersurface k)).toScheme.picardGroup

Stacks.PuncturedSpectrumPicard.QuadricCone.dimension_bound_isSharp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PuncturedSpectrumPicard/QuadricConeExample.lean, line 1228.

The dimension bound in [Stacks, Tag 0F2I] is sharp. For every field k the ring A = k⟦x,y,z,w⟧/(xy - zw) is a Noetherian local complete intersection of dimension exactly three — so it satisfies every hypothesis of [Stacks, Tag 0F2I] except dim A ≥ 4 — and the Picard group of its punctured spectrum is nontrivial.

public theorem dimension_bound_isSharp (k : Type u) [Field k] :
    IsNoetherianRing (hypersurface k) ∧ IsLocalRing (hypersurface k) ∧
      LocalCompleteIntersection.IsCompleteIntersectionRing (hypersurface k) ∧
      ringKrullDim (hypersurface k) = 3 ∧
      ¬ Subsingleton
        (Stacks.Divisors.puncturedSpectrum (hypersurface k)).toScheme.picardGroup

Tag 0F9L, an example

Tag 0F9L in the Stacks Project.

Stacks.PuncturedSpectrumPicard.NonRegularSequence.exists_puncturedSpectrum_firstOrderThickening, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PuncturedSpectrumPicard/NonRegularSequenceExample/PicardGroup.lean, line 635. The attribute's comment: “the punctured spectra: reduction modulo w is a first-order thickening U₀ ⟶ U over Spec of the reduction, invertible global functions lift along it, and its ideal sheaf pulled back to U₀ is the structure sheaf of U₀”.

[Stacks, Tag 0F9L], the punctured spectra. Reduction modulo w is a first-order thickening i : U₀ ⟶ U of the punctured spectrum of A₀ inside that of A, lying over Spec of the reduction q : A → A₀; every invertible global function on U₀ is the restriction of one on U; and the ideal sheaf of i, pulled back to U₀, is the structure sheaf of U₀.

These are the source's three geometric inputs. The thickening is A = A₀[w]/(w²) read on spectra and restricted to the punctured spectra; the lifting of units is the section ι of q together with Γ(U₀, 𝒪_{U₀}) = A₀; and the identification of the ideal sheaf is multiplication by w, which carries A₀ isomorphically onto the kernel wA of q.

public theorem exists_puncturedSpectrum_firstOrderThickening (k : Type u) [Field k] :
    ∃ (q : exampleRing k →+* intermediateRing k)
      (i : (Stacks.Divisors.puncturedSpectrum (intermediateRing k)).toScheme ⟶
        (Stacks.Divisors.puncturedSpectrum (exampleRing k)).toScheme)
      (_ : Stacks.Thickenings.IsFirstOrderThickening i),
      (∀ p : powerSeriesRing k 8,
        q (Ideal.Quotient.mk (eightVariableIdeal k) p) =
          Ideal.Quotient.mk (sevenVariableIdeal k) (MvPowerSeries.killCompl sevenToEight p)) ∧
      i ≫ (Stacks.Divisors.puncturedSpectrum (exampleRing k)).ι =
        (Stacks.Divisors.puncturedSpectrum (intermediateRing k)).ι ≫
          Spec.map (CommRingCat.ofHom q) ∧
      Function.Surjective (Stacks.Thickenings.unitsToSubCohomology i 0) ∧
      Nonempty ((SheafOfModules.toSheaf
        (Stacks.Divisors.puncturedSpectrum (intermediateRing k)).toScheme.ringCatSheaf).obj
          (SheafOfModules.unit
            (Stacks.Divisors.puncturedSpectrum (intermediateRing k)).toScheme.ringCatSheaf) ≅
        Stacks.Thickenings.idealAddSheafOnSub i)

Stacks.PuncturedSpectrumPicard.NonRegularSequence.exampleRing_scheme_picardGroup_puncturedSpectrum_not_subsingleton, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PuncturedSpectrumPicard/NonRegularSequenceExample/PicardGroup.lean, line 773. The attribute's comment: “the conclusion: the Picard group of the punctured spectrum is nontrivial, at the same Scheme.picardGroup that Stacks 0F2I is stated at, so this is literally the negation of that proposition's conclusion for this A”.

[Stacks, Tag 0F9L], the conclusion. The Picard group of the punctured spectrum U = Spec A ∖ {𝔪} of A = k⟦a,b,x,y,z,u,v,w⟧/(a³, b³, xa² + yab + zb², w²) is nontrivial. Together with powerSeriesRing_isRegularLocalRing and powerSeriesRing_dimension — the ambient ring B = k⟦a,b,x,y,z,u,v,w⟧ is regular of dimension 8, and A = B/(f₁, f₂, f₃, f₄) with r = 4, so dim B - r = 4 ≥ 4 — this is the source's witness that [Stacks, Tag 0F2I] fails without the hypothesis that f₁, …, f_r be a regular sequence.

The Picard group is AlgebraicGeometry.Scheme.picardGroup, the same one [Stacks, Tag 0F2I] and the companion example Stacks.PuncturedSpectrumPicard.QuadricCone.picardGroup_not_subsingleton' are stated at, so this is literally the negation of that proposition's conclusion for this A.

The argument itself runs in the universe-shrunk model of Tag 040B, where the exact sequence of [Stacks, Tag 0C6R] lives: it is exampleRing_picardGroup_puncturedSpectrum_not_subsingleton', carried here across Stacks.SheafOfModules.picardGroupShrinkAddEquiv, the isomorphism of abelian groups between the two models.

public theorem exampleRing_scheme_picardGroup_puncturedSpectrum_not_subsingleton
    (k : Type u) [Field k] :
    ¬ Subsingleton
      (Stacks.Divisors.puncturedSpectrum (exampleRing k)).toScheme.picardGroup

Stacks.PuncturedSpectrumPicard.NonRegularSequence.socleRing_nontrivial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PuncturedSpectrumPicard/NonRegularSequenceExample/Rings.lean, line 116. The attribute's comment: “nontrivial five-variable quotient”.

Stacks 0F9L (nontrivial five-variable quotient). The ring A₁ = k⟦a,b,x,y,z⟧/(a³, b³, xa² + yab + zb²) is nonzero.

public theorem socleRing_nontrivial (k : Type u) [Field k] :
    Nontrivial (socleRing k)

Stacks.PuncturedSpectrumPicard.NonRegularSequence.intermediateRing_nontrivial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PuncturedSpectrumPicard/NonRegularSequenceExample/Rings.lean, line 144. The attribute's comment: “nontrivial seven-variable quotient”.

Stacks 0F9L (nontrivial seven-variable quotient). The ring A₀ = k⟦a,b,x,y,z,u,v⟧/(a³, b³, xa² + yab + zb²) is nonzero.

public theorem intermediateRing_nontrivial (k : Type u) [Field k] :
    Nontrivial (intermediateRing k)

Stacks.PuncturedSpectrumPicard.NonRegularSequence.exampleRing_nontrivial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PuncturedSpectrumPicard/NonRegularSequenceExample/Rings.lean, line 172. The attribute's comment: “nontrivial eight-variable quotient”.

Stacks 0F9L (nontrivial eight-variable quotient). The ring A = k⟦a,b,x,y,z,u,v,w⟧/(a³, b³, xa² + yab + zb², w²) is nonzero.

public theorem exampleRing_nontrivial (k : Type u) [Field k] :
    Nontrivial (exampleRing k)

Stacks.PuncturedSpectrumPicard.NonRegularSequence.socleElement_ne_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PuncturedSpectrumPicard/NonRegularSequenceExample/Rings.lean, line 190. The attribute's comment: “nonzero socle element”.

Stacks 0F9L (nonzero socle element). The class of a²b² in A₁ = k⟦a,b,x,y,z⟧/(a³, b³, xa² + yab + zb²) is nonzero.

public theorem socleElement_ne_zero (k : Type u) [Field k] :
    socleElement k ≠ 0

Stacks.PuncturedSpectrumPicard.NonRegularSequence.socleElement_mul_variable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PuncturedSpectrumPicard/NonRegularSequenceExample/Rings.lean, line 288. The attribute's comment: “socle element annihilated by all five variables”.

Stacks 0F9L (socle element annihilated by all five variables). The class of a²b² in A₁ = k⟦a,b,x,y,z⟧/(a³, b³, xa² + yab + zb²) is killed by each of the five variables a, b, x, y, z.

public theorem socleElement_mul_variable (k : Type u) [Field k] (i : Fin 5) :
    socleElement k * Ideal.Quotient.mk (fiveVariableIdeal k) (MvPowerSeries.X i) = 0

Stacks.PuncturedSpectrumPicard.NonRegularSequence.socleRing_depth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PuncturedSpectrumPicard/NonRegularSequenceExample/Rings.lean, line 340. The attribute's comment: “depth of the five-variable quotient”.

Stacks 0F9L (depth of the five-variable quotient). The ring A₁ = k⟦a,b,x,y,z⟧/(a³, b³, xa² + yab + zb²) has depth 0 along its maximal ideal.

public theorem socleRing_depth (k : Type u) [Field k] :
    Module.depth (socleRing k) (IsLocalRing.maximalIdeal (socleRing k))
      (socleRing k) = 0

Stacks.PuncturedSpectrumPicard.NonRegularSequence.intermediateRing_depth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PuncturedSpectrumPicard/NonRegularSequenceExample/Rings.lean, line 517. The attribute's comment: “depth of the seven-variable quotient”.

Stacks 0F9L (depth of the seven-variable quotient). The ring A₀ = k⟦a,b,x,y,z,u,v⟧/(a³, b³, xa² + yab + zb²) has depth 2 along its maximal ideal.

public theorem intermediateRing_depth (k : Type u) [Field k] :
    Module.depth (intermediateRing k) (IsLocalRing.maximalIdeal (intermediateRing k))
      (intermediateRing k) = 2

Stacks.PuncturedSpectrumPicard.NonRegularSequence.powerSeriesRing_isRegularLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PuncturedSpectrumPicard/NonRegularSequenceExample/Rings.lean, line 529. The attribute's comment: “regular ambient ring”.

The ambient power-series ring is regular.

public theorem powerSeriesRing_isRegularLocalRing (k : Type u) [Field k] :
    IsRegularLocalRing (powerSeriesRing k 8)

Stacks.PuncturedSpectrumPicard.NonRegularSequence.powerSeriesRing_dimension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PuncturedSpectrumPicard/NonRegularSequenceExample/Rings.lean, line 541. The attribute's comment: “dimension of the ambient ring”.

Stacks 0F9L (dimension of the ambient ring). The power-series ring k⟦a,b,x,y,z,u,v,w⟧ has Krull dimension 8.

public theorem powerSeriesRing_dimension (k : Type u) [Field k] :
    ringKrullDim (powerSeriesRing k 8) = 8

Stacks.PuncturedSpectrumPicard.NonRegularSequence.exampleRing_equiv_truncatedPolynomial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PuncturedSpectrumPicard/NonRegularSequenceExample/SquareZero.lean, line 666. The attribute's comment: “square-zero extension with its chosen coordinates”.

The square-zero description, with the inclusion of A₀ identified with constant polynomials and the chosen eighth variable identified with X.

public theorem exampleRing_equiv_truncatedPolynomial (k : Type u) [Field k] :
    ∃ (e : exampleRing k ≃+* truncatedPolynomialRing k)
      (ι : intermediateRing k →+* exampleRing k)
      (q : exampleRing k →+* intermediateRing k),
      (∀ p : powerSeriesRing k 7,
        ι (Ideal.Quotient.mk (sevenVariableIdeal k) p) =
          Ideal.Quotient.mk (eightVariableIdeal k) (MvPowerSeries.rename sevenToEight p)) ∧
      (∀ p : powerSeriesRing k 8,
        q (Ideal.Quotient.mk (eightVariableIdeal k) p) =
          Ideal.Quotient.mk (sevenVariableIdeal k) (MvPowerSeries.killCompl sevenToEight p)) ∧
      (∀ a : intermediateRing k,
        e (ι a) = Ideal.Quotient.mk _ (Polynomial.C a)) ∧
      e (squareZeroCoordinate k) =
        Ideal.Quotient.mk _ (Polynomial.X : Polynomial (intermediateRing k)) ∧
      (∀ a : intermediateRing k, q (ι a) = a) ∧
      q (squareZeroCoordinate k) = 0 ∧
      Function.Injective (fun a : intermediateRing k => squareZeroCoordinate k * ι a) ∧
      Function.Exact
        (fun a : intermediateRing k => squareZeroCoordinate k * ι a)
        q

Stacks.PuncturedSpectrumPicard.NonRegularSequence.exampleRing_depth, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PuncturedSpectrumPicard/NonRegularSequenceExample/SquareZero.lean, line 714. The attribute's comment: “depth of the eight-variable quotient”.

Stacks 0F9L (depth of the eight-variable quotient). The ring A = k⟦a,b,x,y,z,u,v,w⟧/(a³, b³, xa² + yab + zb², w²) has depth 2 along its maximal ideal.

public theorem exampleRing_depth (k : Type u) [Field k] :
    Module.depth (exampleRing k) (IsLocalRing.maximalIdeal (exampleRing k))
      (exampleRing k) = 2

Stacks.PuncturedSpectrumPicard.NonRegularSequence.intermediateRing_globalSections_puncturedSpectrum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PuncturedSpectrumPicard/NonRegularSequenceExample/SquareZero.lean, line 786. The attribute's comment: “global functions on the punctured spectrum of A₀”.

Depth two identifies the global functions on the seven-variable punctured spectrum with the original quotient, via the canonical restriction map.

public theorem intermediateRing_globalSections_puncturedSpectrum (k : Type u) [Field k] :
    let U := Stacks.Divisors.puncturedSpectrum (intermediateRing k)
    Function.Bijective
      (((Scheme.ΓSpecIso (.of (intermediateRing k))).inv ≫ U.ι.appTop).hom)

Stacks.PuncturedSpectrumPicard.NonRegularSequence.exampleRing_globalSections_puncturedSpectrum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/PuncturedSpectrumPicard/NonRegularSequenceExample/SquareZero.lean, line 797. The attribute's comment: “global functions on the punctured spectrum of A”.

The same global-functions identification for the square-zero quotient.

public theorem exampleRing_globalSections_puncturedSpectrum (k : Type u) [Field k] :
    let U := Stacks.Divisors.puncturedSpectrum (exampleRing k)
    Function.Bijective
      (((Scheme.ΓSpecIso (.of (exampleRing k))).inv ≫ U.ι.appTop).hom)

Sources

LeanStacks.PuncturedSpectrumPicard.picardColimitSurjective · Stacks.PuncturedSpectrumPicard.exists_isCompatible · Stacks.PuncturedSpectrumPicard.exists_isCompatiblePullback_puncturedSpectrum · Stacks.PuncturedSpectrumPicard.picardColimitSurjective_of_isDualizingComplex · Stacks.PuncturedSpectrumPicard.surjective_schemePullbackClass_puncturedClosedFibre_of_isNoetherianRing · Stacks.PuncturedSpectrumPicard.surjective_schemePullbackClass_puncturedClosedFibre · Stacks.PuncturedSpectrumPicard.surjective_schemePullbackClass_puncturedClosedFibre_of_localCohomology · Stacks.AlgebraicGeometry.PicardBaseChange.injective_schemePullbackClass_puncturedSpectrumCompletionMap

Section52.28 Application to Lefschetz theorems #

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

Tag 0EL1, a proposition

Tag 0EL1 in the Stacks Project.

Stacks.Algebraization.isIso_zeroSchemeComparison_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/LefschetzZeroSchemeComparison.lean, line 71. The attribute's comment: “The tower Qₙ is indexed from n = 0 and Qₙ is cut out by the n-th power of the ideal sheaf of Q = Z(s), which is the ideal sheaf of Z(sⁿ); the zeroth term is empty and does not change the limit. Depth and dimension are compared in the extended integers.”.

Stacks Tag 0EL1. Let k be a field, P a proper scheme over k, 𝓛 an ample invertible 𝒪_P-module, s ∈ Γ(P, 𝓛) with zero scheme Q and 𝓕 a coherent 𝒪_P-module. If depth(𝓕_p) + dim({p}‾) > σ at every p ∈ P ∖ Q, then the comparison map Hⁱ(P, 𝓕) → lim Hⁱ(Qₙ, 𝓕ₙ) is an isomorphism for 0 ≤ i < σ.

theorem isIso_zeroSchemeComparison_of_isProper (k : Type u) [Field k] {X : Scheme.{u}}
    (π : X ⟶ Spec (.of k)) [IsProper π] (L : X.Modules) [Stacks.Ample.IsInvertibleModule X L]
    (hL : Stacks.Ample.IsAmple X L) (s : Γ(L, ⊤)) (F : X.Modules) [F.IsCoherent] (σ : ℤ)
    (hdepth : ∀ x : X, x ∉ ((zeroScheme X L s).support : Set X) →
      enatToEInt (sheafDepthAt F x) + krullDimToEInt (dimClosureAt X x) > (σ : EInt))
    (i : ℕ) (hi : (i : ℤ) < σ) :
    haveI : F.IsQuasicoherent := isQuasicoherent_of_isCoherent F
    IsIso (zeroSchemeComparison X L s F i)

Stacks.Algebraization.isIso_zeroSchemeComparison_of_depthAddDim_gt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/SectionPowerAlgebraization.lean, line 244. The attribute's comment: “H^i(P,F) -> lim H^i(Q_n,F_n) is an isomorphism for i < sigma, from depth(F_p) + dim(closure{p}) > sigma off the zero scheme of s; carried: the punctured-cone fibre dichotomy (hsplit, hproj), the section ring data A, I, fam, f, M (clause (1) of 0B5T, hence 02O5/02O6, is absent from this library), and the algebraization square halg identifying the comparison map with that of 0EKM via 0EKH”.

Stacks Project, Tag 0EL1 (Proposition 52.28.1). Let P be a scheme, L an invertible 𝒪_P-module, s a global section of L with zero scheme Q, let Qₙ be the n-th infinitesimal neighbourhood of Q in P, let 𝓕 be a quasi-coherent 𝒪_P-module with restrictions 𝓕ₙ to Qₙ, and let σ be an integer with

depth(𝓕_p) + dim({p}‾) > σ

at every point p of P outside Q. Then Hⁱ(P, 𝓕) ⟶ lim Hⁱ(Qₙ, 𝓕ₙ) is an isomorphism for every 0 ≤ i < σ.

The depth–dimension hypothesis is hdepth and it is the hypothesis of the tag, read with the depth of a module at a point of [Stacks, Tag 0341] part (1) and the dimension of the closure of a point. Three inputs are carried; see the module documentation for why each is unavailable.

hsplit, with hproj: the fibre dichotomy of the punctured cone π|_U, which rests on π|_U being smooth of relative dimension one. This is what transports hdepth from P to Spec A, and hproj says that the primes of A outside V(I) lie over P ∖ Q.

the section ring data A, I, fam, f and M, with A a Noetherian k-algebra of finite type which is f-adically complete and M finite: clause (1) of [Stacks, Tag 0B5T] is not in this library, so the finite generation of the section ring cannot be produced here.

halg: the algebraization square identifying the geometric comparison map with the one of [Stacks, Tag 0EKM].

theorem isIso_zeroSchemeComparison_of_depthAddDim_gt
    (k : Type u) [Field k] (X : Scheme.{u}) (L : X.Modules)
    [Stacks.Ample.IsInvertibleModule X L] (s : Γ(L, ⊤)) (F : X.Modules) [F.IsQuasicoherent]
    (σ : ℕ)
    (hdepth : ∀ x : X, x ∉ ((zeroScheme X L s).support : Set X) →
      enatToEInt (sheafDepthAt F x) + krullDimToEInt (dimClosureAt X x) > ((σ : ℤ) : EInt))
    (A : Type u) [CommRing A] [IsNoetherianRing A] [Algebra k A] [Algebra.FiniteType k A]
    (M : Type u) [AddCommGroup M] [Module A M] [Module.Finite A M]
    (I : Ideal A) (hI : I.FG) {r : ℕ} (fam : Fin r → A)
    (hfam : Ideal.span (Set.range fam) = I) (f : A) (hf : f ∈ I)
    [IsAdicComplete (Ideal.span {f}) A]
    (proj : PrimeSpectrum A → X)
    (hproj : ∀ p : PrimeSpectrum A, p ∉ PrimeSpectrum.zeroLocus (I : Set A) →
      proj p ∉ ((zeroScheme X L s).support : Set X))
    (hsplit : ∀ p : PrimeSpectrum A, p ∉ PrimeSpectrum.zeroLocus (I : Set A) →
      ∀ q : PrimeSpectrum A, q ∈ PrimeSpectrum.zeroLocus (I : Set A) →
      p.asIdeal ≤ q.asIdeal →
      (localizedDepth A M p = sheafDepthAt F (proj p) ∧
          relativeDimAt A p q = dimClosureAt X (proj p) + 1) ∨
        (localizedDepth A M p = sheafDepthAt F (proj p) + 1 ∧
          relativeDimAt A p q = dimClosureAt X (proj p)))
    (halg : ∀ i : ℕ, i < σ →
      ∃ (e₁ : Hgroup X.ringCatSheaf ⊤ i F ≃+
          (complementCohomologyFunctor fam (i : ℤ)).obj (ModuleCat.of A M))
        (e₂ : ↥(limit (IdealTower.cohomologyTower (zeroSchemeTowerIdeal X L s)
            (zeroSchemeTowerIdeal_succ_le X L s) F i)) ≃+
          ↥(Stacks.ProZero.towerSections
            (HigherComplementTower.quotientCohomologyTower fam f (ModuleCat.of A M) (i : ℤ))
            (HigherComplementTower.quotientCohomologyTransition fam f (ModuleCat.of A M)
              (i : ℤ)))),
          ∀ x : Hgroup X.ringCatSheaf ⊤ i F,
            e₂ (zeroSchemeComparison X L s F i x) =
              HigherComplementTower.toTowerSections fam f (ModuleCat.of A M) (i : ℤ) (e₁ x))
    (i : ℕ) (hi : i < σ) :
    IsIso (zeroSchemeComparison X L s F i)

Tag 0EL2, a lemma

Tag 0EL2 in the Stacks Project.

Stacks.Algebraization.isIso_openNeighbourhoodComparison_of_depthAddDim_gt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/SectionPowerAlgebraizationApplications.lean, line 284. The attribute's comment: “Gamma(V,F) -> lim Gamma(Y_n,F_n) is an isomorphism for every open V containing Y = Z(s), from depth(F_x) + dim(closure{x}) > 1 off Y; carried: the input of 0EL1 (hin) and the bijectivity of Gamma(X,F) -> Gamma(V,F) (hV.isIso_Hrestrict)”.

Stacks Project, Tag 0EL2 (Lemma 52.28.2). Let k be a field, X a scheme proper over k, L an ample invertible 𝒪_X-module, s a global section of L, Y = Z(s) its zero scheme with n-th infinitesimal neighbourhood Yₙ = Z(sⁿ), and 𝓕 a coherent 𝒪_X-module with

depth(𝓕_x) + dim({x}‾) > 1

at every x ∈ X ∖ Y. Then Γ(V, 𝓕) ⟶ lim Γ(Yₙ, 𝓕ₙ) is an isomorphism for every open subscheme V ⊆ X containing Y.

The displayed hypothesis is the hypothesis of [Stacks, Tag 0EL1] at σ = 1, and the conclusion for V = X is that tag in degree i = 0 < 1. The map on V is c, characterized — uniquely, restriction being bijective — by its composite with restriction from X being the comparison map of [Stacks, Tag 0EL1].

Two things are carried: the input hin of [Stacks, Tag 0EL1], and the bijectivity of Γ(X, 𝓕) ⟶ Γ(V, 𝓕), which is the field Stacks.Algebraization.OpenNeighbourhoodSections.isIso_Hrestrict and is the whole content of this lemma beyond the proposition; see that structure for the source's argument and for the two library gaps it runs through.

theorem isIso_openNeighbourhoodComparison_of_depthAddDim_gt
    {k : Type u} [Field k] {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of k)) [IsProper fX]
    {L : X.Modules} [Stacks.Ample.IsInvertibleModule X L] (hL : Stacks.Ample.IsAmple X L)
    {s : Γ(L, ⊤)} {F : X.Modules} [F.IsQuasicoherent]
    (hdepth : ∀ x : X, x ∉ ((zeroScheme X L s).support : Set X) →
      enatToEInt (sheafDepthAt F x) + krullDimToEInt (dimClosureAt X x) > ((1 : ℤ) : EInt))
    {A : Type u} [CommRing A] [IsNoetherianRing A] [Algebra k A] [Algebra.FiniteType k A]
    {M : Type u} [AddCommGroup M] [Module A M] [Module.Finite A M]
    {I : Ideal A} {r : ℕ} {fam : Fin r → A} {f : A} [IsAdicComplete (Ideal.span {f}) A]
    {proj : PrimeSpectrum A → X}
    (hin : ZeroSchemeAlgebraizationInput k X L s F 1 A M I fam f proj)
    {V : X.Opens} (hV : OpenNeighbourhoodSections k fX L hL s F V)
    (c : Hgroup X.ringCatSheaf V 0 F ⟶
      limit (IdealTower.cohomologyTower (zeroSchemeTowerIdeal X L s)
        (zeroSchemeTowerIdeal_succ_le X L s) F 0))
    (hc : Hrestrict X.ringCatSheaf (le_top : V ≤ ⊤) 0 F ≫ c = zeroSchemeComparison X L s F 0) :
    IsIso c

Stacks.Algebraization.isIso_openComparison_of_depthAddDim_gt, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/ZeroSchemeOpenNeighbourhood.lean, line 378. The attribute's comment: “Gamma(V,F) -> lim Gamma(Y_n,F_n) is an isomorphism for every open V containing Y = Z(s), for F coherent on X proper over a field with depth(F_x) + dim(closure{x}) > 1 off Y; Gamma is degree-zero cohomology and Y_n is cut out by the n-th power of the ideal of Y”.

Stacks Project, Tag 0EL2 (Lemma 52.28.2). Let k be a field, X a scheme proper over k, L an ample invertible 𝒪_X-module, s a global section of L, Y = Z(s) its zero scheme with n-th infinitesimal neighbourhood Yₙ, and 𝓕 a coherent 𝒪_X-module with depth(𝓕_x) + dim({x}‾) > 1 at every x ∈ X ∖ Y. Then Γ(V, 𝓕) ⟶ lim Γ(Yₙ, 𝓕ₙ) is an isomorphism for every open subscheme V ⊆ X containing Y.

For V = X this is [Stacks, Tag 0EL1] at σ = 1 in degree 0 (Stacks.Algebraization.isIso_zeroSchemeComparison_of_isProper). Restriction from X to V followed by the comparison over V is the comparison over X (Stacks.Algebraization.IdealTower.Hrestrict_comp_openComparison), and restriction is bijective because every point of X ∖ V is closed with depth ≥ 2 there (Stacks.Algebraization.isIso_Hrestrict_zero_of_depthAddDim_gt).

theorem isIso_openComparison_of_depthAddDim_gt (k : Type u) [Field k] {X : Scheme.{u}}
    (fX : X ⟶ Spec (CommRingCat.of k)) [IsProper fX] (L : X.Modules)
    [Stacks.Ample.IsInvertibleModule X L] (hL : Stacks.Ample.IsAmple X L) (s : Γ(L, ⊤))
    (F : X.Modules) [F.IsCoherent]
    (hdepth : ∀ x : X, x ∉ ((zeroScheme X L s).support : Set X) →
      enatToEInt (sheafDepthAt F x) + krullDimToEInt (dimClosureAt X x) > ((1 : ℤ) : EInt))
    (V : X.Opens) (hV : ((zeroScheme X L s).support : Set X) ⊆ V) :
    haveI : F.IsQuasicoherent := isQuasicoherent_of_isCoherent F
    IsIso (IdealTower.openComparison (zeroSchemeTowerIdeal X L s)
      (zeroSchemeTowerIdeal_succ_le X L s) F
      (fun n => (support_zeroSchemeTowerIdeal_subset L s n).trans hV))

Tag 0EL3, an example

Tag 0EL3 in the Stacks Project.

Stacks.Algebraization.isIso_zeroSchemeComparison_zero_of_isCohenMacaulay_surface, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/LefschetzCohenMacaulayVariety.lean, line 193. The attribute's comment: “clause (2): on a Cohen-Macaulay proper surface over k, H^0(X,E) -> lim H^0(Y_n,E_n) is an isomorphism, for E finite locally free and Y the zero scheme of a section of an ample invertible module”.

Stacks Project, Tag 0EL3 (Example 52.28.3), clause (2). Let k be a field, X a proper variety over k, L an ample invertible 𝒪_X-module (the source's 𝒪_X(Y)), s a global section of L with zero scheme Y and n-th infinitesimal neighbourhood Yₙ, and 𝓔 a finite locally free 𝒪_X-module. If X is a Cohen–Macaulay surface, then

H⁰(X, 𝓔) ⟶ lim H⁰(Yₙ, 𝓔ₙ)

is an isomorphism.

theorem isIso_zeroSchemeComparison_zero_of_isCohenMacaulay_surface
    {k : Type u} [Field k] {X : Scheme.{u}} (fX : X ⟶ Spec (.of k)) [IsProperVariety k fX]
    {L : X.Modules} [Stacks.Ample.IsInvertibleModule X L] (hL : Stacks.Ample.IsAmple X L)
    (s : Γ(L, ⊤)) (E : X.Modules)
    [_root_.AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} E]
    (hCM : IsCohenMacaulay X) (hdim : topologicalKrullDim X = 2) :
    haveI := Stacks.AlgebraicGeometry.CoherenceCriteria.isQuasicoherent_of_isFiniteLocallyFree E
    IsIso (zeroSchemeComparison X L s E 0)

Stacks.Algebraization.isIso_zeroSchemeComparison_of_isCohenMacaulay_threefold, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/LefschetzCohenMacaulayVariety.lean, line 214. The attribute's comment: “clause (3): on a Cohen-Macaulay proper threefold over k, H^0(X,E) -> lim H^0(Y_n,E_n) and H^1(X,E) -> lim H^1(Y_n,E_n) are isomorphisms, for E finite locally free and Y the zero scheme of a section of an ample invertible module”.

Stacks Project, Tag 0EL3 (Example 52.28.3), clause (3). In the situation of clause (2), if X is a Cohen–Macaulay threefold then both

H⁰(X, 𝓔) ⟶ lim H⁰(Yₙ, 𝓔ₙ) and H¹(X, 𝓔) ⟶ lim H¹(Yₙ, 𝓔ₙ)

are isomorphisms.

theorem isIso_zeroSchemeComparison_of_isCohenMacaulay_threefold
    {k : Type u} [Field k] {X : Scheme.{u}} (fX : X ⟶ Spec (.of k)) [IsProperVariety k fX]
    {L : X.Modules} [Stacks.Ample.IsInvertibleModule X L] (hL : Stacks.Ample.IsAmple X L)
    (s : Γ(L, ⊤)) (E : X.Modules)
    [_root_.AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} E]
    (hCM : IsCohenMacaulay X) (hdim : topologicalKrullDim X = 3) :
    haveI := Stacks.AlgebraicGeometry.CoherenceCriteria.isQuasicoherent_of_isFiniteLocallyFree E
    IsIso (zeroSchemeComparison X L s E 0) ∧ IsIso (zeroSchemeComparison X L s E 1)

Stacks.Algebraization.isIso_zeroSchemeComparison_zero_of_isNormal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/LefschetzCohenMacaulayVariety.lean, line 239. The attribute's comment: “the normal case: on a normal proper variety over k of dimension at least two (the normal surface of clause (2), the normal threefold of the closing remark), H^0(X,E) -> lim H^0(Y_n,E_n) is an isomorphism”.

Stacks Project, Tag 0EL3 (Example 52.28.3), the normal case. In the situation of clause (2), if X is normal of dimension at least two, then

H⁰(X, 𝓔) ⟶ lim H⁰(Yₙ, 𝓔ₙ)

is an isomorphism. At dimension two this is the source's "for example normal" in clause (2); at dimension three it is the closing remark that on a normal threefold the result holds for H⁰. A normal scheme satisfies (S₂) (Serre's criterion, [Stacks, Tag 031S]), which is the pattern at d = 2.

theorem isIso_zeroSchemeComparison_zero_of_isNormal
    {k : Type u} [Field k] {X : Scheme.{u}} (fX : X ⟶ Spec (.of k)) [IsProperVariety k fX]
    {L : X.Modules} [Stacks.Ample.IsInvertibleModule X L] (hL : Stacks.Ample.IsAmple X L)
    (s : Γ(L, ⊤)) (E : X.Modules)
    [_root_.AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} E]
    [IsNormal X] (hdim : ((2 : ℕ) : WithBot ℕ∞) ≤ topologicalKrullDim X) :
    haveI := Stacks.AlgebraicGeometry.CoherenceCriteria.isQuasicoherent_of_isFiniteLocallyFree E
    IsIso (zeroSchemeComparison X L s E 0)

Stacks.Algebraization.isIso_zeroSchemeComparison_zero_of_cohenMacaulaySurface, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/SectionPowerAlgebraizationApplications.lean, line 360. The attribute's comment: “clause (2): on a Cohen-Macaulay (for example normal) surface, H^0(X,E) -> lim H^0(Y_n,E_n) is an isomorphism; the depth-dimension bound is proved from the Cohen-Macaulay condition and the dimension formula, hin bundles the three inputs of 0EL1”.

Stacks Project, Tag 0EL3 (Example 52.28.3), clause (2). Let k be a field, X a proper variety over k, L an ample invertible 𝒪_X-module — the source's 𝒪_X(Y) — s a global section with zero scheme Y and n-th infinitesimal neighbourhood Yₙ, and 𝓔 a finite locally free 𝒪_X-module. If X is a Cohen–Macaulay surface, for example a normal one, then

H⁰(X, 𝓔) ⟶ lim H⁰(Yₙ, 𝓔ₙ)

is an isomorphism.

This is the general pattern at d = 2, hence σ = 1 and the single degree i = 0: the Cohen–Macaulay condition and the dimension 2 supply the depth–dimension bound through Stacks.Algebraization.intCast_le_sheafDepthAt_add_dimClosureAt_of_isCohenMacaulay. The remaining hypothesis hin is the input of [Stacks, Tag 0EL1].

theorem isIso_zeroSchemeComparison_zero_of_cohenMacaulaySurface
    {k : Type u} [Field k] {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of k))
    [IsProperVariety k fX]
    {L : X.Modules} [Stacks.Ample.IsInvertibleModule X L] {s : Γ(L, ⊤)} {E : X.Modules}
    [E.IsQuasicoherent] [_root_.AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} E]
    (hCM : AlgebraicGeometry.IsCohenMacaulay X)
    (hdim : topologicalKrullDim X = ((2 : ℕ) : WithBot ℕ∞))
    {A : Type u} [CommRing A] [IsNoetherianRing A] [Algebra k A] [Algebra.FiniteType k A]
    {M : Type u} [AddCommGroup M] [Module A M] [Module.Finite A M]
    {I : Ideal A} {r : ℕ} {fam : Fin r → A} {f : A} [IsAdicComplete (Ideal.span {f}) A]
    {proj : PrimeSpectrum A → X}
    (hin : ZeroSchemeAlgebraizationInput k X L s E 1 A M I fam f proj) :
    IsIso (zeroSchemeComparison X L s E 0)

Stacks.Algebraization.isIso_zeroSchemeComparison_of_cohenMacaulayThreefold, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/SectionPowerAlgebraizationApplications.lean, line 390. The attribute's comment: “clause (3): on a Cohen-Macaulay threefold, H^i(X,E) -> lim H^i(Y_n,E_n) is an isomorphism for i = 0 and i = 1; the depth-dimension bound is proved from the Cohen-Macaulay condition and the dimension formula, hin bundles the three inputs of 0EL1”.

Stacks Project, Tag 0EL3 (Example 52.28.3), clause (3). In the situation of clause (2), if X is a Cohen–Macaulay threefold then both

H⁰(X, 𝓔) ⟶ lim H⁰(Yₙ, 𝓔ₙ) and H¹(X, 𝓔) ⟶ lim H¹(Yₙ, 𝓔ₙ)

are isomorphisms.

This is the general pattern at d = 3, hence σ = 2 and the two degrees i = 0, 1. The source's closing remark that a normal threefold still gives H⁰ is the general pattern at d = 2 applied to it: a normal local ring has depth at least min(2, dim), so the bound 2 holds although the dimension is three.

theorem isIso_zeroSchemeComparison_of_cohenMacaulayThreefold
    {k : Type u} [Field k] {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of k))
    [IsProperVariety k fX]
    {L : X.Modules} [Stacks.Ample.IsInvertibleModule X L] {s : Γ(L, ⊤)} {E : X.Modules}
    [E.IsQuasicoherent] [_root_.AlgebraicGeometry.SheafOfModules.IsFiniteLocallyFree.{u, u, u} E]
    (hCM : AlgebraicGeometry.IsCohenMacaulay X)
    (hdim : topologicalKrullDim X = ((3 : ℕ) : WithBot ℕ∞))
    {A : Type u} [CommRing A] [IsNoetherianRing A] [Algebra k A] [Algebra.FiniteType k A]
    {M : Type u} [AddCommGroup M] [Module A M] [Module.Finite A M]
    {I : Ideal A} {r : ℕ} {fam : Fin r → A} {f : A} [IsAdicComplete (Ideal.span {f}) A]
    {proj : PrimeSpectrum A → X}
    (hin : ZeroSchemeAlgebraizationInput k X L s E 2 A M I fam f proj)
    (i : ℕ) (hi : i < 2) :
    IsIso (zeroSchemeComparison X L s E i)

Tag 0EL4, a lemma

Tag 0EL4 in the Stacks Project.

Stacks.Algebraization.exists_finite_graded_proIso_completion_of_canonicallyExtends, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/GradedAlgebraization.lean, line 744.

Stacks Project, Tag 0EL4. In the algebraization situation (Situation 0EHC) let A be graded with irrelevant ideal 𝔞 = A₊ and I homogeneous, let (ℱₙ) be an object of Coh(U, I𝒪_U) presented as (M̃ₙ|_U) by an inverse system (Mₙ) of graded A-modules, and suppose (ℱₙ) extends canonically to X = Spec(A). Then there is a finite graded A-module N such that

(a) the inverse systems (N/IⁿN) and (Mₙ) are pro-isomorphic in the category of graded A-modules modulo A₊-power torsion modules, and

(b) (ℱₙ) is the completion of the coherent module associated to N.

The category of graded A-modules modulo A₊-power torsion modules is the localization of GradedModuleCat at the maps with A₊-power torsion kernel and cokernel (GradedModuleCat.isoModTorsion), and the pro-objects of the two inverse systems composed with the localization functor are presented as colimits of representables, as in Stacks.ProObject.hasProLadder. The systems are indexed from 0: the term n of (Mₙ) and of (ℱₙ) is the source's term n + 1, and the term n of the adic quotients is N/Iⁿ⁺¹N (GradedModuleCat.adicQuotients). The coherent module associated to N is restricted to U before completing, (ℱₙ) living on U.

The restriction maps Mₙ → Γ(U, ℱₙ) become isomorphisms in the quotient category, and (Γ(U, ℱₙ)) is linked to (N/Iⁿ⁺¹N) by a ladder of degree-preserving maps (Stacks.Algebraization.exists_finite_graded_ladder_of_canonicallyExtends), which is a pro-isomorphism of graded modules (Stacks.ProObject.nonempty_colimitYonedaIso_of_hasProLadder) and stays one after localizing.

public theorem exists_finite_graded_proIso_completion_of_canonicallyExtends
    (S : AlgebraizationSituation.{u})
    {σ : Type v} [SetLike σ S.A] [AddSubgroupClass σ S.A] {𝒜 : ℕ → σ} [GradedRing 𝒜]
    (hirr : S.a = (HomogeneousIdeal.irrelevant 𝒜).toIdeal) (hIhom : S.I.IsHomogeneous 𝒜)
    (M : ℕᵒᵖ ⥤ GradedModuleCat.{u, u, v} 𝒜)
    (F : Stacks.Coherent.CoherentAdicSystems (idealOnOpen S))
    (hpres : Nonempty (F.obj ≅ M ⋙ GradedModuleCat.toModuleCat 𝒜 ⋙ tilde.functor (.of S.A) ⋙
      Scheme.Modules.restrictFunctor S.U.ι))
    (hext : CanonicallyExtends S F) :
    ∃ (N : GradedModuleCat.{u, u, v} 𝒜) (hN : Module.Finite S.A N.carrier),
      Nonempty (colimit ((GradedModuleCat.adicQuotients 𝒜 N S.I hIhom ⋙
          (GradedModuleCat.isoModTorsion 𝒜 (HomogeneousIdeal.irrelevant 𝒜).toIdeal).Q).op ⋙
            yoneda) ≅
        colimit ((M ⋙
          (GradedModuleCat.isoModTorsion 𝒜 (HomogeneousIdeal.irrelevant 𝒜).toIdeal).Q).op ⋙
            yoneda)) ∧
      Nonempty ((completionFunctor S.U.toScheme (idealOnOpen S)).obj
          (restrictCoherentModules S.U.ι
            (tildeCoherentModule S (ModuleCat.of S.A N.carrier) hN)) ≅ F)

Stacks.Algebraization.exists_finite_graded_algebraization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/LefschetzGradedAlgebraization.lean, line 161. The attribute's comment: “(a) and (b); graded Gm-descent (0EKL) and the 0BK0 comparison hypothesised”.

In the algebraization situation of a graded ring A whose irrelevant ideal is 𝔞 and whose ideal I is homogeneous, let (Mₙ) be the inverse system of graded modules presenting a coherent formal module on U, let (Nₙ) be the graded inverse system attached to its canonical extension, and let (Mₙ) → (Nₙ) be a degree-preserving comparison with 𝔞-power torsion kernel and cokernel. Then there is a finite graded A-module N with N/IⁿN ≃ Nₙ compatibly with the transition maps, and (Mₙ) maps to the inverse system (N/IⁿN) by degree-preserving maps with 𝔞-power torsion kernel and cokernel.

public theorem exists_finite_graded_algebraization (S : AlgebraizationSituation.{u})
    {σ : Type v} [SetLike σ S.A] [AddSubmonoidClass σ S.A] {𝒜 : ℕ → σ} [GradedRing 𝒜]
    (hirr : S.a = (HomogeneousIdeal.irrelevant 𝒜).toIdeal) (hIhom : S.I.IsHomogeneous 𝒜)
    {M : ℕ → Type w} [∀ n, AddCommGroup (M n)] [∀ n, Module S.A (M n)]
    (ℳ : ∀ n, ℤ → AddSubgroup (M n)) [∀ n, DirectSum.Decomposition (ℳ n)]
    (s : ∀ n, M (n + 1) →ₗ[S.A] M n)
    {N : ℕ → Type w} [∀ n, AddCommGroup (N n)] [∀ n, Module S.A (N n)]
    [∀ n, Module.Finite S.A (N n)]
    (𝒩 : ∀ n, ℤ → AddSubgroup (N n)) [∀ n, DirectSum.Decomposition (𝒩 n)]
    (h𝒩 : ∀ (n i : ℕ) (d : ℤ) (a : S.A) (x : N n), a ∈ 𝒜 i → x ∈ 𝒩 n d → a • x ∈ 𝒩 n (i + d))
    (t : ∀ n, N (n + 1) →ₗ[S.A] N n)
    (ht : ∀ (n : ℕ) (d : ℤ) (x : N (n + 1)), x ∈ 𝒩 (n + 1) d → t n x ∈ 𝒩 n d)
    (htsurj : ∀ n, Function.Surjective (t n))
    (htker : ∀ n, LinearMap.ker (t n) = S.I ^ n • (⊤ : Submodule S.A (N (n + 1))))
    (c : ∀ n, M n →ₗ[S.A] N n)
    (hc : ∀ (n : ℕ) (d : ℤ) (x : M n), x ∈ ℳ n d → c n x ∈ 𝒩 n d)
    (hcs : ∀ n, (t n).comp (c (n + 1)) = (c n).comp (s n))
    (hcker : ∀ n, IsIPowerTorsion S.A (LinearMap.ker (c n)) S.a)
    (hccoker : ∀ n, IsIPowerTorsion S.A (N n ⧸ LinearMap.range (c n)) S.a) :
    ∃ (P : Type w) (_ : AddCommGroup P) (_ : Module S.A P) (𝒬 : ℤ → AddSubgroup P)
        (_ : DirectSum.Decomposition 𝒬)
        (e : ∀ n, (P ⧸ S.I ^ n • (⊤ : Submodule S.A P)) ≃ₗ[S.A] N n)
        (g : ∀ n, M n →ₗ[S.A] P ⧸ S.I ^ n • (⊤ : Submodule S.A P)),
      Module.Finite S.A P ∧
      (∀ (i : ℕ) (d : ℤ) (a : S.A) (x : P), a ∈ 𝒜 i → x ∈ 𝒬 d → a • x ∈ 𝒬 (i + d)) ∧
      (∀ (n : ℕ) (d : ℤ) (x : P), x ∈ 𝒬 d → e n (Submodule.Quotient.mk x) ∈ 𝒩 n d) ∧
      (∀ (n : ℕ) (x : P),
        t n (e (n + 1) (Submodule.Quotient.mk x)) = e n (Submodule.Quotient.mk x)) ∧
      (∀ (n : ℕ) (x : M n), e n (g n x) = c n x) ∧
      (∀ (n : ℕ) (d : ℤ) (x : M n), x ∈ ℳ n d →
        ∃ p ∈ 𝒬 d, g n x = Submodule.Quotient.mk p) ∧
      (∀ (n : ℕ) (x : M (n + 1)) (p : P), g (n + 1) x = Submodule.Quotient.mk p →
        g n (s n x) = Submodule.Quotient.mk p) ∧
      (∀ n, IsIPowerTorsion S.A (LinearMap.ker (g n)) S.a) ∧
      (∀ n, IsIPowerTorsion S.A
        ((P ⧸ S.I ^ n • (⊤ : Submodule S.A P)) ⧸ LinearMap.range (g n)) S.a)

Tag 0EL5, a proposition

Tag 0EL5 in the Stacks Project.

Stacks.Algebraization.satisfiesDepthInequalities_one_two_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/DepthInequalitiesCohomologicalDimensionOne.lean, line 464. The attribute's comment: “only the opening step, as an equivalence: the depth hypothesis is the (1, 2)-inequalities, this library's encoding of conditions (b), (c), (d) of 0EJF at d = 1; in the affine Situation 0EHC, with the distance function for dim(closure q) and with cd(A, I) = 1 hypothesised; the conclusion that the system is a completion is not proved”.

In Situation 0EHC let (ℱ_n) be an object of Coh(U, I𝒪_U) and assume cd(A, I) = 1. Then (ℱ_n) satisfies the (1, 2)-inequalities if and only if

depth((ℱ_y^∧)_𝔭) + dim(𝒪_{X,y}^∧/𝔭) + δ^Y_Z(y) > 2

for every y ∈ U ∩ Y and every prime 𝔭 ⊆ 𝒪_{X,y}^∧ with 𝔭 ∉ V(I𝒪_{X,y}^∧).

public theorem satisfiesDepthInequalities_one_two_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 1 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 > ((2 : ℤ) : EInt)

Stacks.Algebraization.isCompletionOfCoherent_of_two_lt_depth_add_dim, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/LefschetzFormalModuleAlgebraization.lean, line 68.

Let k be a field, P a proper scheme over k, 𝓛 an ample invertible 𝒪_P-module, s ∈ Γ(P, 𝓛) and 𝓘 the ideal of the zero scheme Q = Z(s). Let (𝓕ₙ) be an object of Coh(P, 𝓘) such that for all q ∈ Q and all primes 𝔭 of 𝒪_{P,q}^∧ not containing 𝓘_q^∧, depth((𝓕_q^∧)_𝔭) + dim(𝒪_{P,q}^∧/𝔭) + dim({q}‾) > 2. Then (𝓕ₙ) is the completion of a coherent 𝒪_P-module.

theorem isCompletionOfCoherent_of_two_lt_depth_add_dim
    (F : Stacks.Coherent.CoherentAdicSystems (zeroScheme P L s))
    (hdepth : ∀ q ∈ (zeroScheme P L s).support,
      ∀ p : PrimeSpectrum (completedLocalRing (zeroScheme P L s) q),
        ¬ completedLocalIdeal (zeroScheme P L s) q ≤ p.asIdeal →
        (2 : EInt) < enatToEInt (completedStalkDepth (zeroScheme P L s) F q p) +
          krullDimToEInt (ringKrullDim (completedLocalRing (zeroScheme P L s) q ⧸ p.asIdeal)) +
          krullDimToEInt (dimClosureAt P q)) :
    haveI : IsLocallyNoetherian P := LocallyOfFiniteType.isLocallyNoetherian fP
    IsCompletionOfCoherent (zeroScheme P L s) F

Tag 0EL6, an example

Tag 0EL6 in the Stacks Project.

Stacks.Algebraization.not_two_lt_completedStalkDepth_of_dim_le_two, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/LefschetzSerreConditionAlgebraization.lean, line 139. The attribute's comment: “clause (1): for a curve or a surface the inequality of 0EL5 fails at every point of Y with nonzero completed stalk and every prime off the completed ideal”.

Let X be a proper variety over a field with an effective Cartier divisor Y whose sheaf 𝒪_X(Y) is ample, and let (𝓔ₙ) be an object of Coh(X, 𝓘) whose terms are finite locally free over the infinitesimal neighbourhoods. If X is a curve or a surface, the hypothesis

depth((𝓔_q^∧)_𝔭) + dim(𝒪_{X,q}^∧/𝔭) + dim({q}‾) > 2

of Stacks 0EL5 fails at every point q of Y where the completed stalk is nonzero and every prime 𝔭 of 𝒪_{X,q}^∧.

theorem not_two_lt_completedStalkDepth_of_dim_le_two (f : X ⟶ Spec (.of k))
    [IsProperVariety k f] (Y : X.IdealSheafData)
    [Stacks.Divisors.IsEffectiveCartierDivisor Y]
    (_hample : AlgebraicGeometry.Scheme.Modules.IsAmple X (Stacks.Divisors.divisorSheaf Y))
    (E : Stacks.Coherent.CoherentAdicSystems Y) (hfree : IsFiniteLocallyFreeAdic Y E)
    (hdim : topologicalKrullDim X ≤ ((2 : ℕ) : WithBot ℕ∞))
    {q : X} (hq : q ∈ Y.support) [Nontrivial (completedStalk Y E q)]
    (p : PrimeSpectrum (completedLocalRing Y q)) :
    ¬ (2 : EInt) < enatToEInt (completedStalkDepth Y E q p) +
      krullDimToEInt (ringKrullDim (completedLocalRing Y q ⧸ p.asIdeal)) +
      krullDimToEInt (dimClosureAt X q)

Stacks.Algebraization.exists_completion_iso_of_hasPropertySk_three, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/LefschetzSerreConditionAlgebraization.lean, line 201. The attribute's comment: “clause (3) with the closing remark: dim X >= 3 and X is (S_3); the freeness of E_n is read over the infinitesimal neighbourhoods Y_n”. References: SGA 2 X (2.2), “(ii)”; SGA 2 XII (3.1), “special case”; SGA 2 XII (3.4), “Clause b), special case”.

Let X be a proper variety over a field k, Y ⊂ X an effective Cartier divisor such that 𝒪_X(Y) is ample, with ideal sheaf 𝓘, and (𝓔ₙ) an object of Coh(X, 𝓘) whose terms are finite locally free over the infinitesimal neighbourhoods. If dim(X) ≥ 3 and X is (S₃), then (𝓔ₙ) is the completion of a coherent 𝒪_X-module 𝓔, and 𝓔 is finite locally free on an open neighbourhood of Y.

theorem exists_completion_iso_of_hasPropertySk_three (f : X ⟶ Spec (.of k))
    [IsProperVariety k f] (Y : X.IdealSheafData) [Stacks.Divisors.IsEffectiveCartierDivisor Y]
    (hample : AlgebraicGeometry.Scheme.Modules.IsAmple X (Stacks.Divisors.divisorSheaf Y))
    (E : Stacks.Coherent.CoherentAdicSystems Y) (hfree : IsFiniteLocallyFreeAdic Y E)
    (hdim : ((3 : ℕ) : WithBot ℕ∞) ≤ topologicalKrullDim X) :
    haveI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian f
    HasPropertySk X 3 →
      ∃ G : AlgebraicGeometry.SheafOfModules.CoherentModules X.ringCatSheaf,
        Nonempty (((completionFunctor X Y).obj G).obj ≅ E.obj) ∧
          ∃ V : X.Opens, (Y.support : Set X) ⊆ (V : Set X) ∧
            AlgebraicGeometry.Scheme.Modules.IsFiniteLocallyFree
              (Scheme.Modules.restrict (show X.Modules from G.obj) V.ι)

Stacks.Algebraization.exists_completion_iso_of_isCohenMacaulay_of_dim_eq_three, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/LefschetzSerreConditionAlgebraization.lean, line 239. The attribute's comment: “clause (2) with the closing remark: X a Cohen-Macaulay threefold; the freeness of E_n is read over the infinitesimal neighbourhoods Y_n”.

In the situation of exists_completion_iso_of_hasPropertySk_three, if X is a Cohen–Macaulay threefold then (𝓔ₙ) is the completion of a coherent 𝒪_X-module 𝓔, finite locally free on an open neighbourhood of Y.

theorem exists_completion_iso_of_isCohenMacaulay_of_dim_eq_three (f : X ⟶ Spec (.of k))
    [IsProperVariety k f] (Y : X.IdealSheafData) [Stacks.Divisors.IsEffectiveCartierDivisor Y]
    (hample : AlgebraicGeometry.Scheme.Modules.IsAmple X (Stacks.Divisors.divisorSheaf Y))
    (E : Stacks.Coherent.CoherentAdicSystems Y) (hfree : IsFiniteLocallyFreeAdic Y E)
    (hCM : AlgebraicGeometry.IsCohenMacaulay X)
    (hdim : topologicalKrullDim X = ((3 : ℕ) : WithBot ℕ∞)) :
    haveI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian f
    ∃ G : AlgebraicGeometry.SheafOfModules.CoherentModules X.ringCatSheaf,
      Nonempty (((completionFunctor X Y).obj G).obj ≅ E.obj) ∧
        ∃ V : X.Opens, (Y.support : Set X) ⊆ (V : Set X) ∧
          AlgebraicGeometry.Scheme.Modules.IsFiniteLocallyFree
            (Scheme.Modules.restrict (show X.Modules from G.obj) V.ι)

Stacks.Algebraization.isCompletionOfCoherent_of_hasPropertySk_three, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/LefschetzSerreConditionSpecialCases.lean, line 213. The attribute's comment: “clause (3): dim X >= 3 and (S_3); the freeness of E_n is corrected to be read over Y_n, since over O_X it would force E_n = 0; 0EL5's conclusion and 0A21 hypothesised”.

Stacks Project, Tag 0EL6, clause (3). Let X be a proper variety over a field with an effective Cartier divisor Y whose sheaf 𝒪_X(Y) is ample, and let (𝓔ₙ) be an object of Coh(X, 𝓘) whose terms are finite locally free over the infinitesimal neighbourhoods. If dim(X) ≥ 3 and X satisfies (S₃), then (𝓔ₙ) is the completion of a coherent 𝒪_X-module.

public theorem isCompletionOfCoherent_of_hasPropertySk_three (f : X ⟶ Spec (.of k))
    [IsProperVariety k f] [IsLocallyNoetherian X] (Y : X.IdealSheafData)
    [Stacks.Divisors.IsEffectiveCartierDivisor Y]
    (_hample : AlgebraicGeometry.Scheme.Modules.IsAmple X (Stacks.Divisors.divisorSheaf Y))
    (E : Stacks.Coherent.CoherentAdicSystems Y)
    (_hfree : IsFiniteLocallyFreeAdic Y E)
    (hdim : ((3 : ℕ) : WithBot ℕ∞) ≤ topologicalKrullDim X) (hS₃ : HasPropertySk X 3)
    (hform : ∀ x : X,
      ringKrullDim (X.presheaf.stalk x) + dimClosureAt X x = topologicalKrullDim X)
    (halgebraize : (∀ x : X, x ∉ Y.support →
        ((2 : ℕ) : WithBot ℕ∞) < localDepthAddDimClosure X x) → IsCompletionOfCoherent Y E) :
    IsCompletionOfCoherent Y E

Stacks.Algebraization.isCompletionOfCoherent_of_isCohenMacaulay_threefold, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/LefschetzSerreConditionSpecialCases.lean, line 232. The attribute's comment: “clause (2): a Cohen-Macaulay threefold; the freeness of E_n is corrected to be read over Y_n, since over O_X it would force E_n = 0; 0EL5 and 0A21 hypothesised”.

Stacks Project, Tag 0EL6, clause (2). In the situation of clause (3), a Cohen–Macaulay threefold satisfies (S₃) and has dimension 3, so (𝓔ₙ) is again the completion of a coherent 𝒪_X-module.

public theorem isCompletionOfCoherent_of_isCohenMacaulay_threefold (f : X ⟶ Spec (.of k))
    [IsProperVariety k f] [IsLocallyNoetherian X] (Y : X.IdealSheafData)
    [Stacks.Divisors.IsEffectiveCartierDivisor Y]
    (_hample : AlgebraicGeometry.Scheme.Modules.IsAmple X (Stacks.Divisors.divisorSheaf Y))
    (E : Stacks.Coherent.CoherentAdicSystems Y)
    (_hfree : IsFiniteLocallyFreeAdic Y E)
    (hCM : AlgebraicGeometry.IsCohenMacaulay X)
    (hdim : topologicalKrullDim X = ((3 : ℕ) : WithBot ℕ∞))
    (hform : ∀ x : X,
      ringKrullDim (X.presheaf.stalk x) + dimClosureAt X x = topologicalKrullDim X)
    (halgebraize : (∀ x : X, x ∉ Y.support →
        ((2 : ℕ) : WithBot ℕ∞) < localDepthAddDimClosure X x) → IsCompletionOfCoherent Y E) :
    IsCompletionOfCoherent Y E

Stacks.Algebraization.exists_isFiniteLocallyFree_neighbourhood_of_isCompletionOfCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/LefschetzSerreConditionSpecialCases.lean, line 280. The attribute's comment: “closing remark: such an E is finite locally free near Y”.

Stacks Project, Tag 0EL6, the closing remark. If the object (𝓔ₙ) is the completion of a coherent 𝒪_X-module 𝓔, then 𝓔 is finite locally free on an open neighbourhood of Y.

At a point y of Y the terms of the system identify the adic quotients 𝓔_y / 𝓘_y ^ (n + 1) 𝓔_y with the stalks of finite locally free modules on the infinitesimal neighbourhoods, hence make them free over 𝒪_{X,y} / 𝓘_y ^ (n + 1) (Stacks.Algebraization.free_quotient_stalk_of_pushforward_iso); a module with a free tower of adic quotients over a Noetherian local ring is free (Stacks.FreeOfAdicQuotients.free_of_forall_free_quotient_pow_smul_top), so 𝓔_y is a finite free 𝒪_{X,y}-module. Stacks 0B8J spreads a free stalk to a free neighbourhood, and those neighbourhoods cover a neighbourhood of Y.

public theorem exists_isFiniteLocallyFree_neighbourhood_of_isCompletionOfCoherent
    (f : X ⟶ Spec (.of k)) [IsProperVariety k f] [IsLocallyNoetherian X] (Y : X.IdealSheafData)
    [Stacks.Divisors.IsEffectiveCartierDivisor Y]
    (_hample : AlgebraicGeometry.Scheme.Modules.IsAmple X (Stacks.Divisors.divisorSheaf Y))
    (E : Stacks.Coherent.CoherentAdicSystems Y)
    (hfree : IsFiniteLocallyFreeAdic Y E)
    (G : AlgebraicGeometry.SheafOfModules.CoherentModules X.ringCatSheaf)
    (hcompletion : Nonempty (((completionFunctor X Y).obj G).obj ≅ E.obj)) :
    ∃ V : X.Opens, (Y.support : Set X) ⊆ (V : Set X) ∧ ∀ x : X, x ∈ V →
      ∃ (U : X.Opens) (_ : x ∈ U) (_ : U ≤ V) (ρ : Type u) (_ : Finite ρ),
        Nonempty (Scheme.Modules.restrict G.obj U.ι ≅ SheafOfModules.free.{u} ρ)

Tag 0EL7, a proposition

Tag 0EL7 in the Stacks Project.

Stacks.Algebraization.isCompletionEquivalence_of_two_lt_depth_add_dimClosure, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Algebraization/LefschetzAmpleSectionCompletionEquivalence.lean, line 121. The attribute's comment: “essential surjectivity up to V; full faithfulness over X; 0EL5, 0EL2 assumed”.

Stacks Project, Tag 0EL7. Let X be a proper scheme over a field, 𝓛 an ample invertible 𝒪_X-module, s ∈ Γ(X, 𝓛) and Y = Z(s) with sheaf of ideals 𝓘. If depth(𝒪_{X,x}) + dim({x}‾) > 2 at every point off Y, then completion along 𝓘 is fully faithful on finite locally free coherent modules, and every finite locally free object of Coh(X, 𝓘) is the completion of a coherent module finite locally free near Y.

public theorem isCompletionEquivalence_of_two_lt_depth_add_dimClosure (k : Type u) [Field k]
    (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) [IsProper f] [IsLocallyNoetherian X] (L : X.Modules)
    [Stacks.Ample.IsInvertibleModule X L] (_hample : Stacks.Ample.IsAmple X L) (s : Γ(L, ⊤))
    (hdepth : ∀ x : X, x ∉ ((zeroScheme X L s).support : Set X) →
      ((2 : ℕ) : WithBot ℕ∞) < localDepthAddDimClosure X x)
    (hff : CompletionFullyFaithfulOnFiniteLocallyFree X (zeroScheme X L s))
    (halgebraize : ∀ F : Stacks.Coherent.CoherentAdicSystems (zeroScheme X L s),
      (∀ n : ℕ, AlgebraicGeometry.Scheme.Modules.IsFiniteLocallyFree (F.obj.obj (op n))) →
      (∀ x : X, x ∉ ((zeroScheme X L s).support : Set X) →
        ((2 : ℕ) : WithBot ℕ∞) < localDepthAddDimClosure X x) →
      ∃ G : AlgebraicGeometry.SheafOfModules.CoherentModules X.ringCatSheaf,
        Nonempty (((completionFunctor X (zeroScheme X L s)).obj G).obj ≅ F.obj) ∧
          ∀ y ∈ ((zeroScheme X L s).support : Set X),
            ∃ (U : X.Opens) (_ : y ∈ U) (ρ : Type u) (_ : Finite ρ),
              Nonempty (Scheme.Modules.restrict G.obj U.ι ≅ SheafOfModules.free.{u} ρ)) :
    IsCompletionEquivalenceOnFiniteLocallyFree X (zeroScheme X L s)

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

Let k be a field, X a proper scheme over k, 𝓛 an ample invertible 𝒪_X-module, s ∈ Γ(X, 𝓛), Y = Z(s) its zero scheme with sheaf of ideals 𝓘, and 𝒱 the open subschemes of X containing Y. Assume depth(𝒪_{X,x}) + dim({x}‾) > 2 for all x ∈ X ∖ Y. Then the completion functor colim_𝒱 Coh(𝒪_V) ⟶ Coh(X, 𝓘) is an equivalence on the full subcategories of finite locally free objects: it lands in the finite locally free objects, it is fully faithful on finite locally free objects, and every finite locally free object of Coh(X, 𝓘) is the completion of a finite locally free coherent module on some V ∈ 𝒱. See the module documentation for how each half is written.

public theorem completionEquivalence_finiteLocallyFree_of_two_lt_depth_add_dimClosure
    (k : Type u) [Field k] (X : Scheme.{u}) (f : X ⟶ Spec (.of k)) [IsProper f]
    (L : X.Modules) [Stacks.Ample.IsInvertibleModule X L] (hL : Stacks.Ample.IsAmple X L)
    (s : Γ(L, ⊤))
    (hdepth : ∀ x : X, x ∉ ((zeroScheme X L s).support : Set X) →
      ((2 : ℕ) : WithBot ℕ∞) < localDepthAddDimClosure X x) :
    letI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian f
    (∀ (V : X.Opens), ((zeroScheme X L s).support : Set X) ⊆ (V : Set X) →
        ∀ G : AlgebraicGeometry.SheafOfModules.CoherentModules V.toScheme.ringCatSheaf,
          AlgebraicGeometry.Scheme.Modules.IsFiniteLocallyFree G.obj →
          IsFiniteLocallyFreeAdic ((zeroScheme X L s).comap V.ι)
            ((completionFunctor V.toScheme ((zeroScheme X L s).comap V.ι)).obj G)) ∧
      NeighbourhoodCompletion.CompletionFullyFaithfulComplete (zeroScheme X L s).subschemeι ∧
      (∀ F : Stacks.Coherent.CoherentAdicSystems (zeroScheme X L s),
        IsFiniteLocallyFreeAdic (zeroScheme X L s) F →
        ∃ (V : X.Opens) (_ : ((zeroScheme X L s).support : Set X) ⊆ (V : Set X))
          (G : AlgebraicGeometry.SheafOfModules.CoherentModules X.ringCatSheaf),
          AlgebraicGeometry.Scheme.Modules.IsFiniteLocallyFree
              (restrictCoherentModules V.ι G).obj ∧
            Nonempty (((completionFunctor X (zeroScheme X L s)).obj G).obj ≅ F.obj) ∧
            Nonempty (((completionFunctor V.toScheme ((zeroScheme X L s).comap V.ι)).obj
                (restrictCoherentModules V.ι G)).obj ≅
              F.obj ⋙ Scheme.Modules.restrictFunctor V.ι))

Sources

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

52.25 Coherent triples to 52.28 Application to Lefschetz…

Section52.25 Coherent triples#

Tag 0F23, a lemma

Tag 0F24, an equation

Tag 0F25, a lemma

Tag 0F26, a lemma

Tag 0F27, a proposition

Tag 0F28, a lemma

Sources

Section52.26 Invertible modules on punctured spectra, I#

Tag 0F2A, a lemma

Tag 0F2B, a proposition

Tag 0FIX, a remark

Sources

Section52.27 Invertible modules on punctured spectra, II#

Tag 0F2D, a lemma

Tag 0F2E, a remark

Tag 0F2F, a lemma

Tag 0F2G, a lemma

Tag 0F2H, a lemma

Tag 0F2I, a proposition

Tag 0F2J, an example

Tag 0F9L, an example

Sources

Section52.28 Application to Lefschetz theorems#

Tag 0EL1, a proposition

Tag 0EL2, a lemma

Tag 0EL3, an example

Tag 0EL4, a lemma

Tag 0EL5, a proposition

Tag 0EL6, an example

Tag 0EL7, a proposition

Sources

Section52.25 Coherent triples #

Section52.26 Invertible modules on punctured spectra, I #

Section52.27 Invertible modules on punctured spectra, II #

Section52.28 Application to Lefschetz theorems #