51.15 Improving coherent modules to 51.22 A bit of uniformity, III

Section51.15 Improving coherent modules#

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

Tag 0DX3, a lemma

Tag 0DX3 in the Stacks Project.

AlgebraicGeometry.depthOneQuotient_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/DepthOneQuotient/Basic.lean, line 948. The attribute's comment: “depth_one_quotient”.

The canonical quotient is coherent, surjective, unchanged away from T, and of depth at least one along T.

public theorem depthOneQuotient_spec (X : Scheme.{u}) [IsNoetherian X]
    (T : Set X) (hT : StableUnderSpecialization T)
    (F : X.Modules) [F.IsCoherent] :
    IsDepthOneQuotient T (toDepthOneQuotient X T hT F)

AlgebraicGeometry.depthOneQuotient_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/DepthOneQuotient/Basic.lean, line 978. The attribute's comment: “depth_one_quotient”.

Every other quotient satisfying the defining properties is uniquely isomorphic to the canonical one over its source.

public theorem depthOneQuotient_unique (X : Scheme.{u}) [IsNoetherian X]
    (T : Set X) (hT : StableUnderSpecialization T)
    (F : X.Modules) [F.IsCoherent]
    (G : X.Modules) (g : F ⟶ G) (hg : IsDepthOneQuotient T g) :
    ∃! e : depthOneQuotient X T hT F ≅ G,
      toDepthOneQuotient X T hT F ≫ e.hom = g

AlgebraicGeometry.isDepthOneQuotient_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Divisors/DepthOneQuotient/FlatPullback.lean, line 186. The attribute's comment: “flat_pullback”. References: EGA IV (5.9.4), “Noetherian, coherent F”.

For a flat morphism f : Y ⟶ X of Noetherian schemes, the pullback of the canonical depth-one quotient of a coherent module along a specialization-closed set T is a depth-one quotient along f ⁻¹' T.

public theorem isDepthOneQuotient_pullback
    {X Y : Scheme.{u}} [IsNoetherian X] [IsNoetherian Y]
    (f : Y ⟶ X) [Flat f]
    (T : Set X) (hT : StableUnderSpecialization T)
    (F : X.Modules) [F.IsCoherent] :
    IsDepthOneQuotient (f.base ⁻¹' T)
      ((Scheme.Modules.pullback f).map
        (toDepthOneQuotient X T hT F))

Tag 0DX4, a lemma

Tag 0DX4 in the Stacks Project.

AlgebraicGeometry.existsUnique_iso_pullback_pushforward_restrict_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/FlatPullbackDepth.lean, line 172. The attribute's comment: “flat pullback compatibility: the pullback of the canonical map is the canonical map for the inverse image of U”.

For a flat morphism f : Y ⟶ X of Noetherian schemes, f^*F → f^*j_*(F|_U) is the canonical extension map for the open subscheme f^{-1}(U) ⊆ Y: there is a unique isomorphism between f^*j_*(F|_U) and j'_*((f^*F)|_{f^{-1}(U)}) compatible with the two canonical maps out of f^*F.

public theorem existsUnique_iso_pullback_pushforward_restrict_flat
    {X Y : Scheme.{u}} [IsNoetherian X] [IsNoetherian Y]
    (f : Y ⟶ X) [Flat f] (F : X.Modules) [F.IsCoherent]
    (U : X.Opens)
    [((Scheme.Modules.pushforward U.ι).obj
      ((Scheme.Modules.pullback U.ι).obj F)).IsCoherent] :
    ∃! e : (Scheme.Modules.pullback f).obj
        ((Scheme.Modules.pushforward U.ι).obj
          ((Scheme.Modules.pullback U.ι).obj F)) ≅
        (Scheme.Modules.pushforward (f ⁻¹ᵁ U).ι).obj
          ((Scheme.Modules.pullback (f ⁻¹ᵁ U).ι).obj
            ((Scheme.Modules.pullback f).obj F)),
      (Scheme.Modules.pullback f).map
        ((Scheme.Modules.pullbackPushforwardAdjunction U.ι).unit.app F) ≫ e.hom =
        (Scheme.Modules.pullbackPushforwardAdjunction (f ⁻¹ᵁ U).ι).unit.app
          ((Scheme.Modules.pullback f).obj F)

AlgebraicGeometry.isCoherent_pushforward_restrict_pullback_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/FlatPullbackDepth.lean, line 197. The attribute's comment: “flat pullback compatibility: the coherence hypothesis of the source holds again for the inverse image of U, so the lemma applies verbatim downstairs”.

For a flat morphism f : Y ⟶ X of Noetherian schemes, the coherence hypothesis of [Stacks, Tag 0DX4] holds again downstairs: j'_*((f^*F)|_{f^{-1}(U)}) is a coherent 𝒪_Y-module. With f^*F coherent (AlgebraicGeometry.isCoherent_pullback), [Stacks, Tag 0DX4] therefore applies to f : Y ⟶ X, f^{-1}(U) and f^*F.

public theorem isCoherent_pushforward_restrict_pullback_of_flat
    {X Y : Scheme.{u}} [IsNoetherian X] [IsNoetherian Y]
    (f : Y ⟶ X) [Flat f] (F : X.Modules) [F.IsCoherent]
    (U : X.Opens)
    [((Scheme.Modules.pushforward U.ι).obj
      ((Scheme.Modules.pullback U.ι).obj F)).IsCoherent] :
    ((Scheme.Modules.pushforward (f ⁻¹ᵁ U).ι).obj
      ((Scheme.Modules.pullback (f ⁻¹ᵁ U).ι).obj
        ((Scheme.Modules.pullback f).obj F))).IsCoherent

AlgebraicGeometry.isIso_pullback_map_unit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/OpenExtension.lean, line 130. The attribute's comment: “clause (1) for the canonical map: it restricts to an isomorphism over U”.

The canonical map F → j_*(F|_U) becomes an isomorphism after restriction to the open subscheme U.

This is the left unitality triangle of the pullback--pushforward adjunction together with invertibility of its counit along an open immersion.

public theorem isIso_pullback_map_unit {X : Scheme.{u}} (F : X.Modules) (U : X.Opens) :
    IsIso ((Scheme.Modules.pullback U.ι).map
      ((Scheme.Modules.pullbackPushforwardAdjunction U.ι).unit.app F))

AlgebraicGeometry.two_le_depth_stalk_pushforward_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/OpenExtension.lean, line 145. The attribute's comment: “clause (2) for the canonical map: the extension has depth at least two outside U”.

The stalks of the extension F' = j_*(F|_U) of a module along an open subscheme have depth at least two at every point outside U.

The module F' is canonically the pushforward of its own restriction to U, by AlgebraicGeometry.isIso_unit_app_pushforward, so the bound is [Stacks, Tag 0EY0] part (3) for the open immersion U.ι, which is Stacks.AlgebraicGeometry.PushforwardRegularity.two_le_depth_stalk_of_isIso_unit_of_notMem. Only finite type of F' is used, so coherence of F is not assumed.

public theorem two_le_depth_stalk_pushforward_restrict
    (X : Scheme.{u}) [IsNoetherian X] (F : X.Modules) (U : X.Opens)
    [((Scheme.Modules.pushforward U.ι).obj
      ((Scheme.Modules.pullback U.ι).obj F)).IsCoherent] :
    ∀ x : X, x ∉ (U : Set X) →
      let F' := (Scheme.Modules.pushforward U.ι).obj ((Scheme.Modules.pullback U.ι).obj F)
      letI : Module (X.presheaf.stalk x)
          (TopCat.Presheaf.stalk (C := Ab.{u}) F'.val.presheaf x) :=
        PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
          F'.val x
      (2 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
        (IsLocalRing.maximalIdeal (X.presheaf.stalk x))
        (TopCat.Presheaf.stalk (C := Ab.{u}) F'.val.presheaf x)

AlgebraicGeometry.unique_iso_pushforward_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/OpenExtension.lean, line 169. The attribute's comment: “uniqueness under the original module”.

A coherent module carrying a map from F which becomes an isomorphism over the open subscheme U and whose stalks have depth at least two outside U is uniquely isomorphic, under F, to the extension j_*(F|_U) of the restriction of F.

public theorem unique_iso_pushforward_restrict
    (X : Scheme.{u}) [IsNoetherian X] (F G : X.Modules)
    [F.IsCoherent] [G.IsCoherent] (U : X.Opens)
    [((Scheme.Modules.pushforward U.ι).obj
      ((Scheme.Modules.pullback U.ι).obj F)).IsCoherent]
    (φ : F ⟶ G)
    (hφ : IsIso ((Scheme.Modules.pullback U.ι).map φ))
    (hdepth : ∀ x : X, x ∉ (U : Set X) →
      let M := TopCat.Presheaf.stalk (C := Ab.{u}) G.val.presheaf x
      letI : Module (X.presheaf.stalk x) M :=
        PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
          G.val x
      (2 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
        (IsLocalRing.maximalIdeal (X.presheaf.stalk x)) M) :
    ∃! e : G ≅ (Scheme.Modules.pushforward U.ι).obj
      ((Scheme.Modules.pullback U.ι).obj F),
      φ ≫ e.hom = (Scheme.Modules.pullbackPushforwardAdjunction U.ι).unit.app F

AlgebraicGeometry.flat_pullback_coherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/OpenExtension.lean, line 195. The attribute's comment: “flat pullback coherence”.

The pullback of the extension j_*(F|_U) along a flat morphism is coherent.

Flatness of f is not needed: coherence of a pullback needs only a locally Noetherian source, by [Stacks, Tag 0EBF].

public theorem flat_pullback_coherent
    {X Y : Scheme.{u}} [IsNoetherian X] [IsNoetherian Y]
    (f : Y ⟶ X) [Flat f] (F : X.Modules) [F.IsCoherent]
    (U : X.Opens)
    [((Scheme.Modules.pushforward U.ι).obj
      ((Scheme.Modules.pullback U.ι).obj F)).IsCoherent] :
    ((Scheme.Modules.pullback f).obj
      ((Scheme.Modules.pushforward U.ι).obj
        ((Scheme.Modules.pullback U.ι).obj F))).IsCoherent

Tag 0DX5, a lemma

Tag 0DX5 in the Stacks Project.

AlgebraicGeometry.correctedImprovement_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/CorrectedImprovement.lean, line 462. The attribute's comment: “corrected form (conditions corrected so that existence holds; the source's existence clause is false, Stacks.ImprovementCounterexample.not_exists_isImprovement_cexSheaf): the pullback of the corrected map along a Cohen-Macaulay morphism with Noetherian source satisfies (1), (2) and the corrected surjectivity-and-depth-one condition along f^{-1}(Z), and the depth-two condition on the inverse image of the points of Z generalizing no point as in (2)”.

The Cohen–Macaulay pullback under the corrected conditions. Let φ : F ⟶ G satisfy the corrected conditions along Z and let f : Y ⟶ X be a Cohen–Macaulay morphism of Noetherian schemes. Then f^*φ has coherent target, is an isomorphism on stalks off f^{-1}(Z), satisfies condition (2) at the points of f^{-1}(Z) reached from outside f^{-1}(Z) for f^*F and condition (2') at the points generalizing those, intrinsically upstairs; and it has depth at least two at the points of f^{-1}(Z) lying over a point of Z generalizing no reached point.

The last clause is not condition (3) for f^*F: that would ask depth two at every point of f^{-1}(Z) generalizing no point reached upstairs, and it fails already for the open immersion D(w) ⊆ Spec k[u, v, w] of the counterexample: Stacks.ImprovementCounterexample.correctedImprovement_pullback_not_intrinsic.

This is AlgebraicGeometry.isNestedImprovement_pullback for the nested pair NotGeneralizingReached Z F ⊆ Z, with the points reached upstairs placed over points of Z generalizing a reached point by AlgebraicGeometry.notMem_notGeneralizingReached_of_reachedFromOutside_pullback.

public theorem correctedImprovement_pullback {X Y : Scheme.{u}} [IsNoetherian X]
    [IsNoetherian Y] {Z : Set X} {F G : X.Modules} (φ : F ⟶ G)
    (hφ : IsCorrectedImprovement Z φ) (f : Y ⟶ X)
    (hfib : ∀ x : X, IsLocallyNoetherian (f.fiber x)) (hcm : f.IsCohenMacaulay hfib) :
    ((Scheme.Modules.pullback f).obj G).IsCoherent ∧
      (∀ y : Y, y ∉ f.base ⁻¹' Z →
        IsIso ((TopCat.Presheaf.stalkFunctor Ab.{u} y).map
          ((Scheme.Modules.pullback f).map φ).mapPresheaf)) ∧
      (∀ y : Y, y ∈ f.base ⁻¹' Z →
        ReachedFromOutside (f.base ⁻¹' Z) ((Scheme.Modules.pullback f).obj F) y →
        Epi ((TopCat.Presheaf.stalkFunctor Ab.{u} y).map
          ((Scheme.Modules.pullback f).map φ).mapPresheaf) ∧
          (letI : Module (Y.presheaf.stalk y)
              (TopCat.Presheaf.stalk (C := Ab.{u})
                ((Scheme.Modules.pullback f).obj G).val.presheaf y) :=
            PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
              (R := Y.presheaf) ((Scheme.Modules.pullback f).obj G).val y
          Module.depth (Y.presheaf.stalk y) (IsLocalRing.maximalIdeal (Y.presheaf.stalk y))
            (TopCat.Presheaf.stalk (C := Ab.{u})
              ((Scheme.Modules.pullback f).obj G).val.presheaf y) = (1 : ℕ∞))) ∧
      (∀ y : Y, y ∈ f.base ⁻¹' Z →
        ¬ ReachedFromOutside (f.base ⁻¹' Z) ((Scheme.Modules.pullback f).obj F) y →
        GeneralizesReached (f.base ⁻¹' Z) ((Scheme.Modules.pullback f).obj F) y →
        Epi ((TopCat.Presheaf.stalkFunctor Ab.{u} y).map
          ((Scheme.Modules.pullback f).map φ).mapPresheaf) ∧
          (letI : Module (Y.presheaf.stalk y)
              (TopCat.Presheaf.stalk (C := Ab.{u})
                ((Scheme.Modules.pullback f).obj G).val.presheaf y) :=
            PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
              (R := Y.presheaf) ((Scheme.Modules.pullback f).obj G).val y
          (1 : ℕ∞) ≤ Module.depth (Y.presheaf.stalk y)
            (IsLocalRing.maximalIdeal (Y.presheaf.stalk y))
            (TopCat.Presheaf.stalk (C := Ab.{u})
              ((Scheme.Modules.pullback f).obj G).val.presheaf y))) ∧
      (∀ y : Y, y ∈ f.base ⁻¹' Z → ¬ GeneralizesReached Z F (f.base y) →
        letI : Module (Y.presheaf.stalk y)
            (TopCat.Presheaf.stalk (C := Ab.{u})
              ((Scheme.Modules.pullback f).obj G).val.presheaf y) :=
          PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
            (R := Y.presheaf) ((Scheme.Modules.pullback f).obj G).val y
        (2 : ℕ∞) ≤ Module.depth (Y.presheaf.stalk y)
          (IsLocalRing.maximalIdeal (Y.presheaf.stalk y))
          (TopCat.Presheaf.stalk (C := Ab.{u})
            ((Scheme.Modules.pullback f).obj G).val.presheaf y))

AlgebraicGeometry.existsUnique_isCorrectedImprovement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/CorrectedImprovement.lean, line 557. The attribute's comment: “corrected form (conditions corrected so that existence holds): the source's existence clause is false, refuted by Stacks.ImprovementCounterexample.not_exists_isImprovement_cexSheaf; with condition (3) at the points of Z which generalize a point as in (2) without being one replaced by surjectivity on stalks and depth at least one, a map F -> F'' exists and is unique up to a unique isomorphism under F, at exactly the source's hypotheses”.

Stacks Project, Tag 0DX5, corrected form: the conditions corrected so that existence holds. The existence clause of the source is false (Stacks.ImprovementCounterexample.not_exists_isImprovement_cexSheaf). Let X be a Noetherian, universally catenary scheme whose local rings have (S₁) formal fibres, Z ⊆ X closed and F coherent. Then there is a map F ⟶ G satisfying the corrected conditions AlgebraicGeometry.IsCorrectedImprovement along Z — the source's (1), (2) and (3), except that at the points of Z which generalize a point as in (2) without being one, (3) is replaced by surjectivity on stalks and depth at least one — and any two such maps are isomorphic by a unique isomorphism under F.

This is the theorem the source's construction proves once its closed subset is chosen as the closure of the bad locus. Its pullback along a Cohen–Macaulay morphism is AlgebraicGeometry.correctedImprovement_pullback; the source's own conditions, whose existence is characterized by AlgebraicGeometry.exists_isImprovement_iff_two_le_depth_depthOneQuotient, are the primary corrected form, for the reason given in the module docstring.

public theorem existsUnique_isCorrectedImprovement (X : Scheme.{u}) [IsNoetherian X]
    (Z : Set X) (hZ : IsClosed Z) (F : X.Modules) [F.IsCoherent]
    (hX : Scheme.IsUniversallyCatenary X)
    (hFibres : ∀ z : X, ∀ q : PrimeSpectrum (X.presheaf.stalk z),
        HasSerreCondition
          (X.completedLocalRing z ⊗[X.presheaf.stalk z] q.asIdeal.ResidueField) 1) :
    ∃ (G : X.Modules) (φ : F ⟶ G), IsCorrectedImprovement Z φ ∧
      ∀ (H : X.Modules) (ψ : F ⟶ H), IsCorrectedImprovement Z ψ →
        ∃! e : G ≅ H, φ ≫ e.hom = ψ

AlgebraicGeometry.exists_isImprovement_iff_two_le_depth_depthOneQuotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/CorrectedImprovement.lean, line 597. The attribute's comment: “corrected form of the existence clause, which is false as stated (refuted by Stacks.ImprovementCounterexample.not_exists_isImprovement_cexSheaf): at exactly the source's hypotheses, a map F -> F'' satisfying (1), (2) and (3) exists if and only if the depth-one quotient F' of Tag 0DX3 has depth at least two at every point of Z which generalizes a point as in (2) without being one; uniqueness and the Cohen-Macaulay pullback hold as stated”.

Stacks Project, Tag 0DX5, corrected form of the existence clause. The existence clause of the source is false: Stacks.ImprovementCounterexample.not_exists_isImprovement_cexSheaf of ImprovementExistenceCounterexample.lean refutes it for X = Spec k[u, v, w], Z = V(u, v), F = (u, v)~ ⊕ (k[u, v, w]/(u, w))~, with every hypothesis of the source witnessed.

Let X be a Noetherian, universally catenary scheme whose local rings have (S₁) formal fibres, Z ⊆ X closed and F coherent, and let F' be the depth-one quotient of F along Z ([Stacks, Tag 0DX3]). Then a map F ⟶ F'' of coherent modules satisfying conditions (1), (2) and (3) of the source exists if and only if depth(F'_x) ≥ 2 at every point x ∈ Z which generalizes a point as in (2) without being one. In the counterexample this fails at (u, v).

The other assertions of the source hold as stated: uniqueness is AlgebraicGeometry.improvement_unique and the Cohen–Macaulay pullback is AlgebraicGeometry.isImprovement_pullback, so this is [Stacks, Tag 0DX5] with only its existence assertion corrected. The criterion is equivalent to the disjointness criterion of AlgebraicGeometry.existsUnique_improvement_of_disjoint_closure_lowDepthNotReached, and is stated pointwise.

For the forward direction an improvement satisfies the corrected conditions (AlgebraicGeometry.isCorrectedImprovement_of_isImprovement), so it is isomorphic to the map of AlgebraicGeometry.exists_isCorrectedImprovement_and_depth_eq, whose target has the depth of F' at the points in question, and condition (3) bounds that depth below by two. Conversely, under the criterion that map satisfies condition (3) there as well.

public theorem exists_isImprovement_iff_two_le_depth_depthOneQuotient (X : Scheme.{u})
    [IsNoetherian X]
    (Z : Set X) (hZ : IsClosed Z) (F : X.Modules) [F.IsCoherent]
    (hX : Scheme.IsUniversallyCatenary X)
    (hFibres : ∀ z : X, ∀ q : PrimeSpectrum (X.presheaf.stalk z),
        HasSerreCondition
          (X.completedLocalRing z ⊗[X.presheaf.stalk z] q.asIdeal.ResidueField) 1) :
    (∃ (G : X.Modules) (φ : F ⟶ G), IsImprovement Z φ) ↔
      ∀ x : X, x ∈ Z → ¬ ReachedFromOutside Z F x → GeneralizesReached Z F x →
        letI : Module (X.presheaf.stalk x)
            (TopCat.Presheaf.stalk (C := Ab.{u})
              (depthOneQuotient X Z hZ.stableUnderSpecialization F).val.presheaf x) :=
          PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
            (R := X.presheaf) (depthOneQuotient X Z hZ.stableUnderSpecialization F).val x
        (2 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
          (IsLocalRing.maximalIdeal (X.presheaf.stalk x))
          (TopCat.Presheaf.stalk (C := Ab.{u})
            (depthOneQuotient X Z hZ.stableUnderSpecialization F).val.presheaf x)

AlgebraicGeometry.isCoherent_pullback_of_isImprovement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/Improvement.lean, line 167. The attribute's comment: “coherence of the target of the pullback, in the assertion about the pullback along a Cohen-Macaulay morphism”.

The target of the pullback of an improvement along a morphism with locally Noetherian source is again coherent.

public theorem isCoherent_pullback_of_isImprovement {X Y : Scheme.{u}} [IsLocallyNoetherian Y]
    (f : Y ⟶ X) {Z : Set X} {F G : X.Modules} (φ : F ⟶ G) (h : IsImprovement Z φ) :
    ((Scheme.Modules.pullback f).obj G).IsCoherent

AlgebraicGeometry.isIso_stalk_pullback_map_of_isImprovement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/Improvement.lean, line 177. The attribute's comment: “the isomorphism away from the inverse image of the closed subscheme, in the assertion about the pullback along a Cohen-Macaulay morphism”.

The pullback of an improvement along any morphism of schemes is an isomorphism on stalks at every point outside the inverse image of the closed subset.

public theorem isIso_stalk_pullback_map_of_isImprovement {X Y : Scheme.{u}} (f : Y ⟶ X)
    {Z : Set X} {F G : X.Modules} (φ : F ⟶ G) (h : IsImprovement Z φ)
    (y : Y) (hy : y ∉ f.base ⁻¹' Z) :
    IsIso ((TopCat.Presheaf.stalkFunctor Ab.{u} y).map
      ((Scheme.Modules.pullback f).map φ).mapPresheaf)

AlgebraicGeometry.two_le_depth_stalk_pullback_of_notReachedFromOutside, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/ImprovementPullback.lean, line 269. The attribute's comment: “condition (3) for the pullback along a Cohen-Macaulay morphism: depth at least two at a point of the inverse image of Z which is not itself reached from outside that inverse image”.

The depth bound at a point not reached upstairs. Let F → F'' be an improvement of a coherent 𝒪_X-module F along Z and let f : Y ⟶ X be a Cohen–Macaulay morphism of Noetherian schemes. At a point y of f^{-1}(Z) which is not reached from outside f^{-1}(Z) for f^*F, the stalk of f^*F'' has depth at least two.

By AlgebraicGeometry.depth_stalk_pullback_eq the depth upstairs is the depth of the stalk of F'' at f y plus the depth of the fibre of the local ring. If f y is not reached from outside Z the first summand is already at least two. If it is reached, the first summand is exactly one, so it suffices that the fibre have positive depth; a fibre of depth zero would carry the point reaching f y up to a point reaching y, which is excluded by hypothesis.

public theorem two_le_depth_stalk_pullback_of_notReachedFromOutside {X Y : Scheme.{u}}
    [IsNoetherian X] [IsNoetherian Y] {Z : Set X} {F G : X.Modules} [F.IsCoherent] (φ : F ⟶ G)
    (hφ : IsImprovement Z φ) (f : Y ⟶ X)
    (hfib : ∀ x : X, IsLocallyNoetherian (f.fiber x)) (hcm : f.IsCohenMacaulay hfib)
    (y : Y) (hy : y ∈ f.base ⁻¹' Z)
    (hnr : ¬ ReachedFromOutside (f.base ⁻¹' Z) ((Scheme.Modules.pullback f).obj F) y) :
    letI : Module (Y.presheaf.stalk y)
        (TopCat.Presheaf.stalk (C := Ab.{u})
          ((Scheme.Modules.pullback f).obj G).val.presheaf y) :=
      PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
        (R := Y.presheaf) ((Scheme.Modules.pullback f).obj G).val y
    (2 : ℕ∞) ≤ Module.depth (Y.presheaf.stalk y)
      (IsLocalRing.maximalIdeal (Y.presheaf.stalk y))
      (TopCat.Presheaf.stalk (C := Ab.{u})
        ((Scheme.Modules.pullback f).obj G).val.presheaf y)

AlgebraicGeometry.isImprovement_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/ImprovementPullback.lean, line 320. The attribute's comment: “the final assertion: the pullback of the map along a Cohen-Macaulay morphism with Noetherian source satisfies conditions (1), (2) and (3) with respect to the inverse image of the closed subscheme”.

Stacks Project, Tag 0DX5, the assertion about the pullback. The pullback of an improvement of a coherent module along a Cohen–Macaulay morphism of Noetherian schemes is an improvement along the inverse image of the closed subset: it satisfies conditions (1), (2) and (3) with respect to f^{-1}(Z) ⊆ Y.

An improvement along Z is an improvement along the nested pair Z ∖ {reached points} ⊆ Z (AlgebraicGeometry.isNestedImprovement_of_isImprovement), whose pullback is an improvement along the inverse images of that pair (AlgebraicGeometry.isNestedImprovement_pullback). Those inverse images are the pair belonging to f^*F and f^{-1}(Z), because the points of f^{-1}(Z) reached from outside f^{-1}(Z) for f^*F are exactly the points lying over points of Z reached from outside Z for F; that is the content of AlgebraicGeometry.reachedFromOutside_base_of_reachedFromOutside_pullback and AlgebraicGeometry.two_le_depth_stalk_pullback_of_notReachedFromOutside.

public theorem isImprovement_pullback {X Y : Scheme.{u}} [IsNoetherian X] [IsNoetherian Y]
    {Z : Set X} {F G : X.Modules} [F.IsCoherent] (φ : F ⟶ G) (hφ : IsImprovement Z φ) (f : Y ⟶ X)
    (hfib : ∀ x : X, IsLocallyNoetherian (f.fiber x)) (hcm : f.IsCohenMacaulay hfib) :
    IsImprovement (f.base ⁻¹' Z) ((Scheme.Modules.pullback f).map φ)

AlgebraicGeometry.epi_stalk_pullback_of_isImprovement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/ImprovementPullback.lean, line 338. The attribute's comment: “the surjectivity in condition (2) for the pullback along a Cohen-Macaulay morphism”.

The pullback of an improvement along a Cohen–Macaulay morphism of Noetherian schemes is surjective on the stalk at every point of the inverse image of the closed subset which is reached from outside that inverse image: the surjectivity half of condition (2) upstairs.

public theorem epi_stalk_pullback_of_isImprovement {X Y : Scheme.{u}} [IsNoetherian X]
    [IsNoetherian Y] {Z : Set X} {F G : X.Modules} [F.IsCoherent] (φ : F ⟶ G)
    (hφ : IsImprovement Z φ) (f : Y ⟶ X)
    (hfib : ∀ x : X, IsLocallyNoetherian (f.fiber x)) (hcm : f.IsCohenMacaulay hfib)
    (y : Y) (hy : y ∈ f.base ⁻¹' Z)
    (hr : ReachedFromOutside (f.base ⁻¹' Z) ((Scheme.Modules.pullback f).obj F) y) :
    Epi ((TopCat.Presheaf.stalkFunctor Ab.{u} y).map
      ((Scheme.Modules.pullback f).map φ).mapPresheaf)

AlgebraicGeometry.depth_stalk_pullback_eq_one_of_isImprovement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/ImprovementPullback.lean, line 353. The attribute's comment: “the depth equality in condition (2) for the pullback along a Cohen-Macaulay morphism: the depth is exactly one, not merely at least one”.

The target of the pullback of an improvement along a Cohen–Macaulay morphism of Noetherian schemes has stalk of depth exactly one at every point of the inverse image of the closed subset which is reached from outside that inverse image: the depth half of condition (2) upstairs.

public theorem depth_stalk_pullback_eq_one_of_isImprovement {X Y : Scheme.{u}} [IsNoetherian X]
    [IsNoetherian Y] {Z : Set X} {F G : X.Modules} [F.IsCoherent] (φ : F ⟶ G)
    (hφ : IsImprovement Z φ) (f : Y ⟶ X)
    (hfib : ∀ x : X, IsLocallyNoetherian (f.fiber x)) (hcm : f.IsCohenMacaulay hfib)
    (y : Y) (hy : y ∈ f.base ⁻¹' Z)
    (hr : ReachedFromOutside (f.base ⁻¹' Z) ((Scheme.Modules.pullback f).obj F) y) :
    letI : Module (Y.presheaf.stalk y)
        (TopCat.Presheaf.stalk (C := Ab.{u})
          ((Scheme.Modules.pullback f).obj G).val.presheaf y) :=
      PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
        (R := Y.presheaf) ((Scheme.Modules.pullback f).obj G).val y
    Module.depth (Y.presheaf.stalk y) (IsLocalRing.maximalIdeal (Y.presheaf.stalk y))
      (TopCat.Presheaf.stalk (C := Ab.{u})
        ((Scheme.Modules.pullback f).obj G).val.presheaf y) = (1 : ℕ∞)

AlgebraicGeometry.improvement_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/ImprovementUniqueness.lean, line 171. The attribute's comment: “uniqueness of the map F → F'': two maps satisfying conditions (1), (2) and (3) are isomorphic by a unique isomorphism under F”.

Stacks Project, Tag 0DX5, uniqueness. Two improvements of a coherent module along the same closed subset are isomorphic by a unique isomorphism compatible with the two maps.

Each is an improvement along the nested pair NotReachedFromOutside Z F ⊆ Z, a subset determined by Z and F alone, so the comparison is the one of [Stacks, Tag 0EI4]. Neither the universal catenarity of X nor the (S₁) condition on the formal fibres of its local rings is used: those hypotheses of the source enter only its existence proof.

public theorem improvement_unique (X : Scheme.{u}) [IsNoetherian X] (Z : Set X) (hZ : IsClosed Z)
    (F G H : X.Modules) [F.IsCoherent] (φ : F ⟶ G) (ψ : F ⟶ H)
    (hφ : IsImprovement Z φ) (hψ : IsImprovement Z ψ) :
    ∃! e : G ≅ H, φ ≫ e.hom = ψ

Tag 0EI3, a lemma

Tag 0EI3 in the Stacks Project.

AlgebraicGeometry.exists_isDepthTwoExtension_of_isCoherent_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/ClosedStabilizedExtension.lean, line 131. The attribute's comment: “existence for a closed subset, conditional only on coherence of the single pushforward of the restriction of the depth-one quotient to the complement; the hypothesis hext of exists_isDepthTwoExtension_of_isStabilizedOpenExtension, namely a coherent stabilized open extension, is discharged here for a closed subset”.

Stacks Project, Tag 0EI3, existence for a closed subset. A coherent module F on a Noetherian scheme admits a map to a coherent module which is an isomorphism on the stalks away from a closed subset T and whose stalks on T have depth at least two, as soon as the single pushforward j_{V,*}(F'|_V) is coherent — where V is the complement of T and F' is the depth-one quotient of F along T.

Together with AlgebraicGeometry.isStabilizedOpenExtension_unit this replaces the hypothesis hext of AlgebraicGeometry.exists_isDepthTwoExtension_of_isStabilizedOpenExtension, which asks for a coherent stabilized open extension, by coherence of one explicit module: for a closed T no colimit of pushforwards over the opens whose complement lies in T is needed, because the complement of T is itself such an open and is the smallest one.

The remaining hypothesis is not removable; it is where the two hypotheses of [Stacks, Tag 0EI3] absent from AlgebraicGeometry.exists_isDepthTwoExtension — a dualizing complex and a depth bound across the boundary of T — must re-enter. See the implementation notes of this module.

public theorem exists_isDepthTwoExtension_of_isCoherent_pushforward
    (X : Scheme.{u}) [IsNoetherian X] (T : Set X) (hT : IsClosed T) (V : X.Opens)
    (hV : (V : Set X) = Tᶜ) (F : X.Modules) [F.IsCoherent]
    (hcoh : ((Scheme.Modules.pushforward V.ι).obj ((Scheme.Modules.pullback V.ι).obj
      (depthOneQuotient X T hT.stableUnderSpecialization F))).IsCoherent) :
    ∃ (G : X.Modules) (φ : F ⟶ G), IsDepthTwoExtension T φ

AlgebraicGeometry.exists_isDepthTwoExtension_of_locallyHasDualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/ClosedSubsetExistence.lean, line 405. The attribute's comment: “existence along a closed subset, with no hypothesis about extensions or colimits, and at the source's hypotheses: the dualizing hypothesis and the depth hypothesis on immediate specializations, nothing else, the coherence of the single pushforward coming from the source's Faltings criterion Tag 0EFD”.

Stacks Project, Tag 0EI3, existence along a closed subset. Let X be a Noetherian scheme which locally has a dualizing complex, let V be an open of X with complement T — so T is closed — and let F be a coherent 𝒪_X-module such that depth(F_x) ≥ 1 whenever some point of T is an immediate specialization of x ∉ T. Then F admits a depth-two extension along T.

No hypothesis about extensions or colimits is left: the module is the single pushforward j_{V,*}(F'|_V) of the depth-one quotient, which is a stabilized open extension by AlgebraicGeometry.isStabilizedOpenExtension_unit and coherent by isCoherent_pushforward_restrict_depthOneQuotient. The two hypotheses are the source's, and both are necessary. See the module documentation.

public theorem exists_isDepthTwoExtension_of_locallyHasDualizingComplex
    (X : Scheme.{u}) [IsNoetherian X] (T : Set X) (V : X.Opens) (hV : (V : Set X) = Tᶜ)
    (F : X.Modules) [F.IsCoherent]
    (hdual : LocallyHasDualizingComplex X)
    (hdepth : ∀ x z : X, x ∉ T → z ∈ T → TopologicalSpace.IsImmediateSpecialization x z →
      (1 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
        (IsLocalRing.maximalIdeal (X.presheaf.stalk x))
        (TopCat.Presheaf.stalk (C := Ab.{u}) F.val.presheaf x)) :
    ∃ (G : X.Modules) (φ : F ⟶ G), IsDepthTwoExtension T φ

AlgebraicGeometry.exists_isDepthTwoExtension_of_stableUnderSpecialization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/DepthLocusGlue.lean, line 223. The attribute's comment: “existence along a specialization-stable subset, at exactly the source's two hypotheses — the dualizing hypothesis and the depth hypothesis on immediate specializations — with no hypothesis about extensions, colimits, a closed subset of T, or finiteness of an exceptional locus”.

Let X be a Noetherian scheme which locally has a dualizing complex, let T ⊆ X be stable under specialization and let F be a coherent 𝒪_X-module such that depth(F_x) ≥ 1 whenever some point of T is an immediate specialization of x ∉ T. Then F admits a depth-two extension along T.

public theorem exists_isDepthTwoExtension_of_stableUnderSpecialization
    (X : Scheme.{u}) [IsNoetherian X] (T : Set X) (hT : StableUnderSpecialization T)
    (F : X.Modules) [F.IsCoherent] (hdual : LocallyHasDualizingComplex X)
    (hdepth : ∀ x z : X, x ∉ T → z ∈ T → TopologicalSpace.IsImmediateSpecialization x z →
      (1 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
        (IsLocalRing.maximalIdeal (X.presheaf.stalk x))
        (TopCat.Presheaf.stalk (C := Ab.{u}) F.val.presheaf x)) :
    ∃ (G : X.Modules) (φ : F ⟶ G), IsDepthTwoExtension T φ

AlgebraicGeometry.depthTwoExtension_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/DepthTwoExtension.lean, line 464. The attribute's comment: “uniqueness, unconditionally: the subset is arbitrary and no dualizing complex is needed”.

Two depth-two extensions of a module along a subset are isomorphic by a unique isomorphism compatible with the two maps.

public theorem depthTwoExtension_unique
    (X : Scheme.{u}) [IsNoetherian X]
    (T : Set X)
    (F G H : X.Modules) (φ : F ⟶ G) (ψ : F ⟶ H)
    (hφ : IsDepthTwoExtension T φ) (hψ : IsDepthTwoExtension T ψ) :
    ∃! e : G ≅ H, φ ≫ e.hom = ψ

AlgebraicGeometry.exists_isDepthTwoExtension_of_hasDualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/DepthTwoExtensionConstruction.lean, line 480. The attribute's comment: “existence, at the source's hypotheses: X Noetherian with a dualizing complex on an affine open cover, T stable under specialization, F coherent, and depth at least one at the immediate specializations into T from outside T; the witness is the single direct image j_*(F|_{X ∖ Z}) across the closure Z of the low-depth locus, not the source's colimit of pushforwards, and its coherence is proved here from Faltings through Tag 0BJY”.

Existence of the depth-two extension. Let X be a Noetherian scheme which locally has a dualizing complex, let T ⊆ X be stable under specialization and let F be coherent. Assume depth(F_x) ≥ 1 at every immediate specialization x ⤳ x' with x' ∈ T and x ∉ T. Then F admits a map to a coherent module which is an isomorphism on the stalks off T and whose stalks on T have depth at least two.

public theorem exists_isDepthTwoExtension_of_hasDualizingComplex
    (X : Scheme.{u}) [IsNoetherian X] (hdual : HasDualizingComplexOnAffineCover X)
    (T : Set X) (hT : StableUnderSpecialization T) (F : X.Modules) [F.IsCoherent]
    (himm : ∀ x x' : X, IsImmediateSpecialization x x' → x' ∈ T → x ∉ T →
      (1 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
        (IsLocalRing.maximalIdeal (X.presheaf.stalk x)) (F.presheaf.stalk x)) :
    ∃ (G : X.Modules) (φ : F ⟶ G), IsDepthTwoExtension T φ

AlgebraicGeometry.existsUnique_isDepthTwoExtension_of_hasDualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/DepthTwoExtensionConstruction.lean, line 499. The attribute's comment: “the source's unique map, as existence together with uniqueness up to a unique isomorphism under F, at the source's hypotheses”.

Existence and uniqueness of the depth-two extension. Under the hypotheses of AlgebraicGeometry.exists_isDepthTwoExtension_of_hasDualizingComplex there is a map F ⟶ F'' of coherent modules which is an isomorphism on the stalks off T and whose stalks on T have depth at least two, and it is unique: any other such map is carried to it by a unique isomorphism under F.

public theorem existsUnique_isDepthTwoExtension_of_hasDualizingComplex
    (X : Scheme.{u}) [IsNoetherian X] (hdual : HasDualizingComplexOnAffineCover X)
    (T : Set X) (hT : StableUnderSpecialization T) (F : X.Modules) [F.IsCoherent]
    (himm : ∀ x x' : X, IsImmediateSpecialization x x' → x' ∈ T → x ∉ T →
      (1 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
        (IsLocalRing.maximalIdeal (X.presheaf.stalk x)) (F.presheaf.stalk x)) :
    ∃ (G : X.Modules) (φ : F ⟶ G), IsDepthTwoExtension T φ ∧
      ∀ (H : X.Modules) (ψ : F ⟶ H), IsDepthTwoExtension T ψ →
        ∃! e : G ≅ H, φ ≫ e.hom = ψ

AlgebraicGeometry.exists_isDepthTwoExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/DepthTwoExtensionExistence.lean, line 249. The attribute's comment: “existence, conditional on a coherent stabilized open extension of the depth-one quotient along the subset and on Tag 0EY0 part (3)”.

Stacks Project, Tag 0EI3, existence. A coherent module on a Noetherian scheme admits a map to a coherent module which is an isomorphism on the stalks away from a specialization-stable subset and whose stalks on that subset have depth at least two.

Two inputs of the source's proof are carried as hypotheses, because this library does not have them.

• hext asks for the extension of the depth-one quotient of F across T by sections over the opens whose complement lies in T — the colimit of the pushforwards j_{V,*}(F'|_V) — as a coherent module. Its coherence is what the source derives from Faltings' finiteness criterion [Stacks, Tag 0EFD] applied to a dualizing complex, using the hypothesis that X locally has one and the hypothesis on the depth of F at the immediate specializations into T. Those two hypotheses of [Stacks, Tag 0EI3] therefore do not appear here.
• hdepthOutside is [Stacks, Tag 0EY0] part (3), the converse of AlgebraicGeometry.isIso_unit_restrict_pushforward_of_depth_ge_two.

The map itself, the clause away from T and the depth clause on T are proved. See the implementation notes of this module.

public theorem exists_isDepthTwoExtension
    (X : Scheme.{u}) [IsNoetherian X] (T : Set X) (hT : StableUnderSpecialization T)
    (F : X.Modules) [F.IsCoherent]
    (hdepthOutside : ∀ (V : X.Opens) (H : X.Modules), H.IsCoherent →
      IsIso ((Scheme.Modules.pullbackPushforwardAdjunction V.ι).unit.app H) →
      ∀ y : X, y ∉ (V : Set X) →
        letI : Module (X.presheaf.stalk y)
            (TopCat.Presheaf.stalk (C := Ab.{u}) H.val.presheaf y) :=
          PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
            (R := X.presheaf) H.val y
        (2 : ℕ∞) ≤ Module.depth (X.presheaf.stalk y)
          (IsLocalRing.maximalIdeal (X.presheaf.stalk y))
          (TopCat.Presheaf.stalk (C := Ab.{u}) H.val.presheaf y))
    (hext : ∃ (G : X.Modules) (ψ : depthOneQuotient X T hT F ⟶ G),
      IsStabilizedOpenExtension T ψ) :
    ∃ (G : X.Modules) (φ : F ⟶ G), IsDepthTwoExtension T φ

AlgebraicGeometry.depthTwoExtension_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/DepthTwoExtensionPullback.lean, line 48. The attribute's comment: “the Cohen-Macaulay pullback clause, unconditionally”.

The pullback of a depth-two extension along a Cohen–Macaulay morphism of Noetherian schemes is a depth-two extension along the inverse image of the subset.

The hypothesis hfib, that the fibres of f are locally Noetherian, is the one under which AlgebraicGeometry.Scheme.Hom.IsCohenMacaulay is stated; it follows from [IsNoetherian Y] by AlgebraicGeometry.isLocallyNoetherian_fiber.

public theorem depthTwoExtension_pullback
    {X Y : Scheme.{u}} [IsNoetherian X] [IsNoetherian Y]
    (T : Set X) (F G : X.Modules) (φ : F ⟶ G)
    (hφ : IsDepthTwoExtension T φ)
    (f : Y ⟶ X) (hfib : ∀ x : X, IsLocallyNoetherian (f.fiber x))
    (hcm : f.IsCohenMacaulay hfib) :
    IsDepthTwoExtension (f ⁻¹' T) ((Scheme.Modules.pullback f).map φ)

AlgebraicGeometry.exists_isDepthTwoExtension_of_isStabilizedOpenExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/ExistenceDepthOutside.lean, line 66. The attribute's comment: “existence, conditional only on a coherent stabilized open extension of the depth-one quotient along the subset; the other hypothesis of exists_isDepthTwoExtension, namely Tag 0EY0 part (3), is discharged here”.

A coherent module on a Noetherian scheme admits a map to a coherent module which is an isomorphism on the stalks away from a specialization-stable subset and whose stalks on that subset have depth at least two, as soon as the depth-one quotient has a stabilized open extension across the subset.

public theorem exists_isDepthTwoExtension_of_isStabilizedOpenExtension
    (X : Scheme.{u}) [IsNoetherian X] (T : Set X) (hT : StableUnderSpecialization T)
    (F : X.Modules) [F.IsCoherent]
    (hext : ∃ (G : X.Modules) (ψ : depthOneQuotient X T hT F ⟶ G),
      IsStabilizedOpenExtension T ψ) :
    ∃ (G : X.Modules) (φ : F ⟶ G), IsDepthTwoExtension T φ

AlgebraicGeometry.exists_isDepthTwoExtension_of_isClosed_of_subset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/SpecializationStableExistence.lean, line 211. The attribute's comment: “existence along a specialization-stable subset, with no hypothesis about extensions or colimits, and at the source's hypotheses — the dualizing hypothesis and the depth hypothesis on immediate specializations — together with a closed subset of T outside which the depth-one quotient already has depth two on T”.

Stacks Project, Tag 0EI3, existence along a specialization-stable subset. Let X be a Noetherian scheme which locally has a dualizing complex, let T ⊆ X be stable under specialization and let F be a coherent 𝒪_X-module such that depth(F_x) ≥ 1 whenever some point of T is an immediate specialization of x ∉ T. Let Z ⊆ T be closed and such that the depth-one quotient F' of F along T already has depth(F'_x) ≥ 2 at the points of T outside Z. Then F admits a depth-two extension along T.

No hypothesis about extensions or colimits is left, and the depth-two extension is the single pushforward j_{Zᶜ,*}(F'|_{Zᶜ}): for a closed T one may take Z = T, recovering AlgebraicGeometry.exists_isDepthTwoExtension_of_locallyHasDualizingComplex. See the module documentation for the three clauses and for the status of Z itself.

public theorem exists_isDepthTwoExtension_of_isClosed_of_subset
    (X : Scheme.{u}) [IsNoetherian X] (T : Set X) (hT : StableUnderSpecialization T)
    (F : X.Modules) [F.IsCoherent]
    (hdual : LocallyHasDualizingComplex X)
    (hdepth : ∀ x z : X, x ∉ T → z ∈ T → TopologicalSpace.IsImmediateSpecialization x z →
      (1 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
        (IsLocalRing.maximalIdeal (X.presheaf.stalk x))
        (TopCat.Presheaf.stalk (C := Ab.{u}) F.val.presheaf x))
    (Z : Set X) (hZclosed : IsClosed Z) (hZT : Z ⊆ T)
    (hZ : ∀ x : X, x ∈ T → x ∉ Z →
      letI : Module (X.presheaf.stalk x)
          (TopCat.Presheaf.stalk (C := Ab.{u}) (depthOneQuotient X T hT F).val.presheaf x) :=
        PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
          (R := X.presheaf) (depthOneQuotient X T hT F).val x
      (2 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
        (IsLocalRing.maximalIdeal (X.presheaf.stalk x))
        (TopCat.Presheaf.stalk (C := Ab.{u})
          (depthOneQuotient X T hT F).val.presheaf x)) :
    ∃ (G : X.Modules) (φ : F ⟶ G), IsDepthTwoExtension T φ

AlgebraicGeometry.exists_isDepthTwoExtension_of_finite_depthOne_locus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/SpecializationStableExistence.lean, line 285. The attribute's comment: “existence along a specialization-stable subset, with no hypothesis about extensions or colimits, and at the source's hypotheses — the dualizing hypothesis and the depth hypothesis on immediate specializations — together with finiteness of the set of points of T where the depth-one quotient still has depth below two”.

Stacks Project, Tag 0EI3, existence along a specialization-stable subset, from finiteness of the depth-one locus. Same as exists_isDepthTwoExtension_of_isClosed_of_subset, with the closed subset replaced by the hypothesis that the set of points of T where the depth-one quotient F' still has depth below two is finite.

A finite set of points has closed closure — the union of the finitely many closures of its points — and that closure stays inside T because T is stable under specialization. So the finite set's closure is a legitimate Z, and the remaining gap in the existence half of [Stacks, Tag 0EI3] is exactly this finiteness. It is the shape the finiteness theorems about depth take: [Stacks, Tag 0ECN] (AlgebraicGeometry.finite_setOf_depth_eq_and_lt_supportDim) says that on a Noetherian scheme with a dualizing complex a coherent module satisfying Serre's condition (S₁) has only finitely many points with depth(F'_x) = 1 and dim Supp(F'_x) > 1.

public theorem exists_isDepthTwoExtension_of_finite_depthOne_locus
    (X : Scheme.{u}) [IsNoetherian X] (T : Set X) (hT : StableUnderSpecialization T)
    (F : X.Modules) [F.IsCoherent]
    (hdual : LocallyHasDualizingComplex X)
    (hdepth : ∀ x z : X, x ∉ T → z ∈ T → TopologicalSpace.IsImmediateSpecialization x z →
      (1 : ℕ∞) ≤ Module.depth (X.presheaf.stalk x)
        (IsLocalRing.maximalIdeal (X.presheaf.stalk x))
        (TopCat.Presheaf.stalk (C := Ab.{u}) F.val.presheaf x))
    (hfin : {x : X | x ∈ T ∧
      letI : Module (X.presheaf.stalk x)
          (TopCat.Presheaf.stalk (C := Ab.{u}) (depthOneQuotient X T hT F).val.presheaf x) :=
        PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
          (R := X.presheaf) (depthOneQuotient X T hT F).val x
      Module.depth (X.presheaf.stalk x) (IsLocalRing.maximalIdeal (X.presheaf.stalk x))
        (TopCat.Presheaf.stalk (C := Ab.{u})
          (depthOneQuotient X T hT F).val.presheaf x) < (2 : ℕ∞)}.Finite) :
    ∃ (G : X.Modules) (φ : F ⟶ G), IsDepthTwoExtension T φ

Tag 0EI4, a lemma

Tag 0EI4 in the Stacks Project.

AlgebraicGeometry.exists_isNestedImprovement_of_isStabilizedOpenExtension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/ExistenceDepthOutside.lean, line 81. The attribute's comment: “existence, conditional only on a coherent stabilized open extension of the depth-one quotient along T'; the other hypothesis of exists_isNestedImprovement, namely Tag 0EY0 part (3), is discharged here”.

A coherent module on a Noetherian scheme admits an improvement along a nested pair T' ⊆ T of subsets stable under specialization, as soon as the depth-one quotient along T has a stabilized open extension across T'.

public theorem exists_isNestedImprovement_of_isStabilizedOpenExtension
    (X : Scheme.{u}) [IsNoetherian X] (T T' : Set X) (hTT' : T' ⊆ T)
    (hT : StableUnderSpecialization T) (F : X.Modules) [F.IsCoherent]
    (hext : ∃ (G : X.Modules) (ψ : depthOneQuotient X T hT F ⟶ G),
      IsStabilizedOpenExtension T' ψ) :
    ∃ (G : X.Modules) (φ : F ⟶ G), IsNestedImprovement T T' φ

AlgebraicGeometry.nestedImprovement_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/NestedImprovement.lean, line 241. The attribute's comment: “uniqueness, unconditionally: no dualizing complex is needed, no condition on immediate specializations is used, and the inclusion T' ⊆ T is not needed either”.

Stacks Project, Tag 0EI4, uniqueness. Two improvements of a coherent module along the same pair of subsets are isomorphic by a unique isomorphism compatible with the two maps.

Each one factors through the depth-one quotient of its source along T by a depth-two extension along T', so the comparison is the one of [Stacks, Tag 0EI3], transported across the epimorphism onto the depth-one quotient.

public theorem nestedImprovement_unique (X : Scheme.{u}) [IsNoetherian X]
    (T T' : Set X) (hT : StableUnderSpecialization T)
    (F G H : X.Modules) [F.IsCoherent] (φ : F ⟶ G) (ψ : F ⟶ H)
    (hφ : IsNestedImprovement T T' φ) (hψ : IsNestedImprovement T T' ψ) :
    ∃! e : G ≅ H, φ ≫ e.hom = ψ

AlgebraicGeometry.exists_isNestedImprovement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/NestedImprovement.lean, line 275. The attribute's comment: “existence, conditional on a coherent stabilized open extension of the depth-one quotient along T' and on Tag 0EY0 part (3); as for Tag 0EI3 in this library, those two hypotheses replace the dualizing complex and the condition on immediate specializations, which are therefore not assumed”.

Stacks Project, Tag 0EI4, existence. A coherent module on a Noetherian scheme admits an improvement along a nested pair T' ⊆ T of subsets stable under specialization: a map to a coherent module which is an isomorphism on the stalks away from T, is surjective on the stalks with target of depth at least one at the points of T outside T', and has target of depth at least two at the points of T'.

The map is the depth-one quotient of F along T followed by a depth-two extension of that quotient along T', which is the source's construction. The hypotheses hdepthOutside and hext are the two inputs of the source's existence proof which this library does not have; they subsume what the source extracts from the dualizing complex and from the condition on immediate specializations into T', so neither of those two hypotheses of the source appears here. See the implementation notes of this module.

public theorem exists_isNestedImprovement (X : Scheme.{u}) [IsNoetherian X]
    (T T' : Set X) (hTT' : T' ⊆ T) (hT : StableUnderSpecialization T)
    (F : X.Modules) [F.IsCoherent]
    (hdepthOutside : ∀ (V : X.Opens) (H : X.Modules), H.IsCoherent →
      IsIso ((Scheme.Modules.pullbackPushforwardAdjunction V.ι).unit.app H) →
      ∀ y : X, y ∉ (V : Set X) →
        letI : Module (X.presheaf.stalk y)
            (TopCat.Presheaf.stalk (C := Ab.{u}) H.val.presheaf y) :=
          PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
            (R := X.presheaf) H.val y
        (2 : ℕ∞) ≤ Module.depth (X.presheaf.stalk y)
          (IsLocalRing.maximalIdeal (X.presheaf.stalk y))
          (TopCat.Presheaf.stalk (C := Ab.{u}) H.val.presheaf y))
    (hext : ∃ (G : X.Modules) (ψ : depthOneQuotient X T hT F ⟶ G),
      IsStabilizedOpenExtension T' ψ) :
    ∃ (G : X.Modules) (φ : F ⟶ G), IsNestedImprovement T T' φ

AlgebraicGeometry.isCoherent_pullback_of_isNestedImprovement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/NestedImprovement.lean, line 409. The attribute's comment: “coherence of the target of the pullback, in the assertion about the pullback along a Cohen-Macaulay morphism”.

Stacks Project, Tag 0EI4, the pullback clause: coherence of the target. The target of the pullback of an improvement along a morphism with locally Noetherian source is again coherent.

A pullback of a coherent module needs only a locally Noetherian source, so neither flatness nor Cohen-Macaulayness of the morphism is used.

public theorem isCoherent_pullback_of_isNestedImprovement {X Y : Scheme.{u}}
    [IsLocallyNoetherian Y] (f : Y ⟶ X) {T T' : Set X} {F G : X.Modules} (φ : F ⟶ G)
    (hφ : IsNestedImprovement T T' φ) :
    ((Scheme.Modules.pullback f).obj G).IsCoherent

AlgebraicGeometry.isIso_stalk_pullback_of_isNestedImprovement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/NestedImprovement.lean, line 424. The attribute's comment: “condition (1) for the pullback: the isomorphism away from the inverse image of T, in the assertion about the pullback along a Cohen-Macaulay morphism”.

Stacks Project, Tag 0EI4, the pullback clause, condition (1). The pullback of an improvement along any morphism of schemes is an isomorphism on the stalks at every point outside the inverse image of T.

The stalk of a pullback is the base change of the stalk, so a bijective stalk map stays bijective; no hypothesis on the morphism is used.

public theorem isIso_stalk_pullback_of_isNestedImprovement {X Y : Scheme.{u}} (f : Y ⟶ X)
    {T T' : Set X} {F G : X.Modules} (φ : F ⟶ G) (hφ : IsNestedImprovement T T' φ)
    (y : Y) (hy : y ∉ f.base ⁻¹' T) :
    IsIso ((TopCat.Presheaf.stalkFunctor Ab.{u} y).map
      ((Scheme.Modules.pullback f).map φ).mapPresheaf)

AlgebraicGeometry.one_le_depth_stalk_pullback_of_isNestedImprovement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/NestedImprovement.lean, line 441. The attribute's comment: “the depth bound of condition (2) for the pullback, in the assertion about the pullback along a Cohen-Macaulay morphism”.

Stacks Project, Tag 0EI4, the pullback clause, the depth bound of condition (2). The target of the pullback of an improvement along a Cohen-Macaulay morphism of Noetherian schemes has stalks of depth at least one at every point of the inverse image of T lying outside the inverse image of T'.

Only the flatness half of the Cohen-Macaulay hypothesis is used: the depth of the base change of a stalk along a flat local homomorphism is the depth of the stalk plus the depth of the fibre, so the bound downstairs is inherited.

public theorem one_le_depth_stalk_pullback_of_isNestedImprovement {X Y : Scheme.{u}}
    [IsNoetherian X] [IsNoetherian Y] {T T' : Set X} {F G : X.Modules} (φ : F ⟶ G)
    (hφ : IsNestedImprovement T T' φ) (f : Y ⟶ X)
    (hfib : ∀ x : X, IsLocallyNoetherian (f.fiber x)) (hcm : f.IsCohenMacaulay hfib)
    (y : Y) (hy : y ∈ f.base ⁻¹' T) (hy' : y ∉ f.base ⁻¹' T') :
    letI : Module (Y.presheaf.stalk y)
        (TopCat.Presheaf.stalk (C := Ab.{u})
          ((Scheme.Modules.pullback f).obj G).val.presheaf y) :=
      PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
        (R := Y.presheaf) ((Scheme.Modules.pullback f).obj G).val y
    (1 : ℕ∞) ≤ Module.depth (Y.presheaf.stalk y)
      (IsLocalRing.maximalIdeal (Y.presheaf.stalk y))
      (TopCat.Presheaf.stalk (C := Ab.{u})
        ((Scheme.Modules.pullback f).obj G).val.presheaf y)

AlgebraicGeometry.two_le_depth_stalk_pullback_of_isNestedImprovement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/NestedImprovement.lean, line 468. The attribute's comment: “condition (3) for the pullback, in the assertion about the pullback along a Cohen-Macaulay morphism”.

Stacks Project, Tag 0EI4, the pullback clause, condition (3). The target of the pullback of an improvement along a Cohen-Macaulay morphism of Noetherian schemes has stalks of depth at least two at every point of the inverse image of T'.

Only the flatness half of the Cohen-Macaulay hypothesis is used, by the same depth formula along a flat local homomorphism.

public theorem two_le_depth_stalk_pullback_of_isNestedImprovement {X Y : Scheme.{u}}
    [IsNoetherian X] [IsNoetherian Y] {T T' : Set X} {F G : X.Modules} (φ : F ⟶ G)
    (hφ : IsNestedImprovement T T' φ) (f : Y ⟶ X)
    (hfib : ∀ x : X, IsLocallyNoetherian (f.fiber x)) (hcm : f.IsCohenMacaulay hfib)
    (y : Y) (hy' : y ∈ f.base ⁻¹' T') :
    letI : Module (Y.presheaf.stalk y)
        (TopCat.Presheaf.stalk (C := Ab.{u})
          ((Scheme.Modules.pullback f).obj G).val.presheaf y) :=
      PresheafOfModules.instModuleCarrierStalkCommRingCatCarrierAbPresheafOpensCarrier
        (R := Y.presheaf) ((Scheme.Modules.pullback f).obj G).val y
    (2 : ℕ∞) ≤ Module.depth (Y.presheaf.stalk y)
      (IsLocalRing.maximalIdeal (Y.presheaf.stalk y))
      (TopCat.Presheaf.stalk (C := Ab.{u})
        ((Scheme.Modules.pullback f).obj G).val.presheaf y)

AlgebraicGeometry.isNestedImprovement_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/NestedImprovement.lean, line 569. The attribute's comment: “the assertion about the pullback along a Cohen-Macaulay morphism: the pullback satisfies conditions (1), (2) and (3) with respect to the inverse images of the two subsets”.

Stacks Project, Tag 0EI4, the assertion about the pullback. The pullback of an improvement along a Cohen-Macaulay morphism of Noetherian schemes is an improvement along the inverse images of the two subsets.

Coherence of the target and condition (1) need no hypothesis on the morphism at all. Of the Cohen-Macaulay hypothesis only the flatness half is used, for the two depth bounds, by the formula for the change in depth along a flat local homomorphism [Stacks, Tag 0338]; the fibre never has to be identified. Surjectivity in condition (2) is epimorphy on a stalk, which is the vanishing of the stalk of the cokernel, and the pullback preserves cokernels and kills the zero module.

public theorem isNestedImprovement_pullback {X Y : Scheme.{u}} [IsNoetherian X] [IsNoetherian Y]
    {T T' : Set X} {F G : X.Modules} (φ : F ⟶ G) (hφ : IsNestedImprovement T T' φ) (f : Y ⟶ X)
    (hfib : ∀ x : X, IsLocallyNoetherian (f.fiber x)) (hcm : f.IsCohenMacaulay hfib) :
    IsNestedImprovement (f.base ⁻¹' T) (f.base ⁻¹' T')
      ((Scheme.Modules.pullback f).map φ)

AlgebraicGeometry.exists_isNestedImprovement_of_hasDualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/NestedImprovementExistence.lean, line 92. The attribute's comment: “existence, at the hypotheses of the source and no others: Noetherian, locally a dualizing complex in the source's sense that every point has an affine neighbourhood carrying one, T' subset T both stable under specialization, immediate specializations into T' starting in T. Tag 0EI3 existence is composed with Tag 0DX3 here”.

Stacks Project, Tag 0EI4, existence, at the hypotheses of the source. Let X be a Noetherian scheme which locally has a dualizing complex and let T' ⊆ T ⊆ X be stable under specialization and such that every immediate specialization into T' starts in T. Then a coherent 𝒪_X-module F admits a map to a coherent module which is an isomorphism on the stalks away from T, is surjective on the stalks with target of depth at least one at the points of T outside T', and has target of depth at least two at the points of T'.

The map is the depth-one quotient of F along T followed by a depth-two extension of that quotient along T', which is the source's construction: the first step is [Stacks, Tag 0DX3], the second is the existence half of [Stacks, Tag 0EI3] in the form AlgebraicGeometry.exists_isDepthTwoExtension_of_hasDualizingComplex, and the composition is AlgebraicGeometry.isNestedImprovement_depthOneQuotient_comp.

The dualizing hypothesis is AlgebraicGeometry.HasDualizingComplexOnAffineCover, which says every point has an affine open neighbourhood whose ring of sections admits a dualizing complex. That is the source's phrase "locally has a dualizing complex", and it is weaker than AlgebraicGeometry.LocallyHasDualizingComplex, which asks this of every affine open.

public theorem exists_isNestedImprovement_of_hasDualizingComplex
    (X : Scheme.{u}) [IsNoetherian X] (hdual : HasDualizingComplexOnAffineCover X)
    (T T' : Set X) (hTT' : T' ⊆ T)
    (hT : StableUnderSpecialization T) (hT' : StableUnderSpecialization T')
    (himm : ∀ x x' : X, IsImmediateSpecialization x x' → x' ∈ T' → x ∈ T)
    (F : X.Modules) [F.IsCoherent] :
    ∃ (G : X.Modules) (φ : F ⟶ G), IsNestedImprovement T T' φ

AlgebraicGeometry.existsUnique_isNestedImprovement_of_hasDualizingComplex, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/ImprovingCoherentModules/NestedImprovementExistence.lean, line 119. The attribute's comment: “the source's unique map, as existence together with uniqueness up to a unique isomorphism under F, at the hypotheses of the source and no others”.

Stacks Project, Tag 0EI4, the source's unique map. Under the hypotheses of AlgebraicGeometry.exists_isNestedImprovement_of_hasDualizingComplex there is a map F ⟶ F'' of coherent modules which is an isomorphism on the stalks away from T, is surjective on the stalks with target of depth at least one at the points of T outside T', and has target of depth at least two at the points of T'; and it is unique: any other such map is carried to it by a unique isomorphism under F.

This is the source's sentence "there exists a unique map" in one statement. Existence is AlgebraicGeometry.exists_isNestedImprovement_of_hasDualizingComplex and uniqueness is AlgebraicGeometry.nestedImprovement_unique, which needs neither the dualizing complex, nor the condition on immediate specializations, nor T' ⊆ T.

public theorem existsUnique_isNestedImprovement_of_hasDualizingComplex
    (X : Scheme.{u}) [IsNoetherian X] (hdual : HasDualizingComplexOnAffineCover X)
    (T T' : Set X) (hTT' : T' ⊆ T)
    (hT : StableUnderSpecialization T) (hT' : StableUnderSpecialization T')
    (himm : ∀ x x' : X, IsImmediateSpecialization x x' → x' ∈ T' → x ∈ T)
    (F : X.Modules) [F.IsCoherent] :
    ∃ (G : X.Modules) (φ : F ⟶ G), IsNestedImprovement T T' φ ∧
      ∀ (H : X.Modules) (ψ : F ⟶ H), IsNestedImprovement T T' ψ →
        ∃! e : G ≅ H, φ ≫ e.hom = ψ

Sources

• Section 51.15, Tag 0DX2
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.depthOneQuotient_spec · AlgebraicGeometry.depthOneQuotient_unique · AlgebraicGeometry.isDepthOneQuotient_pullback · AlgebraicGeometry.existsUnique_iso_pullback_pushforward_restrict_flat · AlgebraicGeometry.isCoherent_pushforward_restrict_pullback_of_flat · AlgebraicGeometry.isIso_pullback_map_unit · AlgebraicGeometry.two_le_depth_stalk_pushforward_restrict · AlgebraicGeometry.unique_iso_pushforward_restrict

Section51.16 Hartshorne-Lichtenbaum vanishing#

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

Tag 0EB1, a lemma

Tag 0EB1 in the Stacks Project.

Stacks.LocalCohomology.cohomologicalDimension_lt_of_le_of_le_jacobson, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/CohomologicalDimension/Jacobson.lean, line 42.

Let A be a Noetherian ring of dimension d and let I ≤ I' be ideals of A with I' inside the Jacobson radical. If the cohomological dimension of I' is less than d, then the cohomological dimension of I is less than d as well.

theorem cohomologicalDimension_lt_of_le_of_le_jacobson
    (A : Type u) [CommRing A] [IsNoetherianRing A]
    (d : ℕ) (hd : ringKrullDim A = (d : WithBot ℕ∞))
    (I I' : Ideal A) (hII' : I ≤ I') (hI' : I' ≤ Ring.jacobson A)
    (hcd : cohomologicalDimension A I' (Ideal.fg_of_isNoetherianRing I') < (d : ℤ)) :
    cohomologicalDimension A I (Ideal.fg_of_isNoetherianRing I) < (d : ℤ)

Tag 0EB2, a lemma

Tag 0EB2 in the Stacks Project.

Stacks.LocalCohomology.cohomologicalDimension_lt_of_isZero_localCohomologyModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/CohomologicalDimension/HartshorneLichtenbaum.lean, line 363.

Stacks Project, Tag 0EB2 (Hartshorne–Lichtenbaum vanishing). Let A be a Noetherian ring of dimension d and let I ⊆ A be an ideal. If H^d_{V(I)}(M) = 0 for some finite A-module M whose support contains every irreducible component of Spec A of dimension d, then the cohomological dimension of I in A is strictly less than d.

theorem cohomologicalDimension_lt_of_isZero_localCohomologyModule
    (A : Type u) [CommRing A] [IsNoetherianRing A]
    (d : ℕ) (hd : ringKrullDim A = (d : WithBot ℕ∞)) (I : Ideal A)
    (M : ModuleCat.{u} A) [Module.Finite A M]
    (hM : ∀ p : PrimeSpectrum A, IsMinimalPrime p.asIdeal →
      ringKrullDim (A ⧸ p.asIdeal) = (d : WithBot ℕ∞) → p ∈ Module.support A M)
    (hvan : IsZero
      (localCohomologyModule A I (Ideal.fg_of_isNoetherianRing I) M (d : ℤ))) :
    cohomologicalDimension A I (Ideal.fg_of_isNoetherianRing I) < (d : ℤ)

Tag 0EB3, a lemma

Tag 0EB3 in the Stacks Project.

Stacks.LocalCohomology.surjective_smul_top_localCohomologyModule_of_avoidsTopMinimalPrimes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/TopDegreeDivisibility.lean, line 184.

Stacks Project, Tag 0EB3. Let A be a Noetherian ring of Krull dimension d, let I ⊆ A be a finitely generated ideal, let Y = V(I) and let M be a finite A-module. An element f ∈ A lying outside every minimal prime p with dim A/p = d acts surjectively on H^d_Y(M).

The source assumes A local. That is not used: the dimension drop for M/fM and the vanishing above the dimension of the support both hold over an arbitrary Noetherian ring, so the hypothesis is dropped.

theorem surjective_smul_top_localCohomologyModule_of_avoidsTopMinimalPrimes
    (A : Type u) [CommRing A] [IsNoetherianRing A] (d : ℕ) (hd : ringKrullDim A = d) (f : A)
    (hf : ∀ p : PrimeSpectrum A, IsMinimalPrime p.asIdeal →
      ringKrullDim (A ⧸ p.asIdeal) = d → f ∉ p.asIdeal)
    (I : Ideal A) (hI : I.FG) (M : ModuleCat.{max u v} A) [Module.Finite A M] :
    Function.Surjective fun x : localCohomologyModule A I hI M (d : ℤ) => f • x

Tag 0EB4, a lemma

Tag 0EB4 in the Stacks Project.

Stacks.LocalCohomology.cohomologicalDimension_lt_of_isZero_homology_localCohomologyDerived, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/CohomologicalDimension/DualizingComplexVanishing.lean, line 367.

Stacks Project, Tag 0EB4. Let A be a Noetherian local ring of dimension d with a normalized dualizing complex ω_A^•, and let I ⊆ A be an ideal. If H^0_{V(I)}(ω_A^•) = 0, then the cohomological dimension of I is strictly less than d.

Write ω_A = H^{-d}(ω_A^•). Choose f ∈ A outside every minimal prime of dimension d which annihilates H^i(ω_A^•) for i > -d; then f acts as zero on every homology object of U = τ_{≥ -d + 1}ω_A^•, so f • 𝟙_U is nilpotent, and therefore a power of f annihilates H^{-1}_{V(I)}(U). The truncation triangle ω_A[d] → ω_A^• → U gives, after applying RΓ_{V(I)}, the exact sequence H^{-1}_{V(I)}(U) → H^0_{V(I)}(ω_A[d]) → H^0_{V(I)}(ω_A^•) = 0, so that same power of f annihilates H^d_{V(I)}(ω_A). By Stacks 0EB3 multiplication by f is surjective on H^d_{V(I)}(ω_A), whence H^d_{V(I)}(ω_A) = 0, and ω_A is supported at every d-dimensional minimal prime by Stacks 0A7V, so Stacks 0EB2 applies.

theorem cohomologicalDimension_lt_of_isZero_homology_localCohomologyDerived
    (A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    (d : ℕ) (hd : ringKrullDim A = (d : WithBot ℕ∞))
    (K : DerivedCategory (ModuleCat.{u} A))
    (hK : Dualizing.IsNormalizedDualizingComplex.{u, u} K) (I : Ideal A)
    (hvan : IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{u} A) 0).obj
      ((localCohomologyDerived A I (Ideal.fg_of_isNoetherianRing I)).obj K))) :
    cohomologicalDimension A I (Ideal.fg_of_isNoetherianRing I) < (d : ℤ)

Tag 0EB5, a lemma

Tag 0EB5 in the Stacks Project.

Ideal.exists_symbolicPower_le_pow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/HartshorneLichtenbaumVanishing/Basic.lean, line 200.

Stacks Project, Tag 0EB5. Let p be a one-dimensional prime ideal in a complete Noetherian local domain. For every n ≥ 1, some symbolic power p⁽ᵐ⁾, with m ≥ n, is contained in the ordinary power pⁿ.

theorem exists_symbolicPower_le_pow [IsNoetherianRing A] [IsLocalRing A] [IsDomain A]
    [IsAdicComplete (IsLocalRing.maximalIdeal A) A]
    (p : Ideal A) [p.IsPrime] (hp : ringKrullDim (A ⧸ p) = 1)
    (n : ℕ) (hn : 1 ≤ n) :
    ∃ m : ℕ, n ≤ m ∧ Ideal.symbolicPower p m ≤ p ^ n

Tag 0EB6, a proposition

Tag 0EB6 in the Stacks Project.

Stacks.LocalCohomology.cohomologicalDimension_lt_of_minimalPrimes_adicCompletion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/CohomologicalDimension/HartshorneLichtenbaumCompletion.lean, line 501.

Hartshorne–Lichtenbaum vanishing. Let A be a Noetherian local ring with completion A^∧ and let I ⊆ A be an ideal such that dim V(I A^∧ + 𝔭) ≥ 1 for every minimal prime 𝔭 ⊆ A^∧ of dimension dim(A). Then the cohomological dimension of I in A is strictly less than dim(A).

theorem cohomologicalDimension_lt_of_minimalPrimes_adicCompletion
    (A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    (d : ℕ) (hd : ringKrullDim A = (d : WithBot ℕ∞)) (I : Ideal A)
    (h : ∀ q : PrimeSpectrum (AdicCompletion (IsLocalRing.maximalIdeal A) A),
      IsMinimalPrime q.asIdeal →
      ringKrullDim ((AdicCompletion (IsLocalRing.maximalIdeal A) A) ⧸ q.asIdeal) =
        (d : WithBot ℕ∞) →
      (1 : WithBot ℕ∞) ≤
        ringKrullDim ((AdicCompletion (IsLocalRing.maximalIdeal A) A) ⧸
          (I.map (algebraMap A (AdicCompletion (IsLocalRing.maximalIdeal A) A)) +
            q.asIdeal))) :
    cohomologicalDimension A I (Ideal.fg_of_isNoetherianRing I) < (d : ℤ)

Tag 0EB7, a lemma

Tag 0EB7 in the Stacks Project.

Stacks.LocalCohomology.cohomologicalDimension_lt_of_isExcellent_of_isNormalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/CohomologicalDimension/HartshorneLichtenbaumExcellent.lean, line 123. The attribute's comment: “cd(A, I) < dim(A)”.

[Stacks Project, Tag 0EB7]. Let A be an excellent normal Noetherian local ring of dimension d and let I ⊆ A be an ideal with dim V(I) ≥ 1. Then the cohomological dimension of I in A is strictly less than d.

theorem cohomologicalDimension_lt_of_isExcellent_of_isNormalRing
    (A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    (hA : IsExcellent A) (hnormal : IsNormalRing A)
    (d : ℕ) (hd : ringKrullDim A = (d : WithBot ℕ∞)) (I : Ideal A)
    (hI : (1 : WithBot ℕ∞) ≤ ringKrullDim (A ⧸ I)) :
    cohomologicalDimension A I (Ideal.fg_of_isNoetherianRing I) < (d : ℤ)

Stacks.LocalCohomology.isAffineOpen_complZeroLocusOpen_of_isExcellent_of_isNormalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/CohomologicalDimension/HartshorneLichtenbaumExcellent.lean, line 149. The attribute's comment: “Spec(A) ∖ V(I) is affine when dim(A) = 2”.

[Stacks Project, Tag 0EB7]. For an excellent normal Noetherian local ring A of dimension two and an ideal I ⊆ A with dim V(I) ≥ 1, the open Spec A ∖ V(I) is affine.

The cohomological dimension bound gives cd(A, I) ≤ 1, hence the vanishing of the cohomology of every quasi-coherent module on the complement in degrees ≥ 1 by Stacks 0DX7; the complement is quasi-compact, so Serre's criterion applies. This is the route of Stacks 0DXD.

theorem isAffineOpen_complZeroLocusOpen_of_isExcellent_of_isNormalRing
    (A : Type u) [CommRing A] [IsNoetherianRing A] [IsLocalRing A]
    (hA : IsExcellent A) (hnormal : IsNormalRing A)
    (hd : ringKrullDim A = (2 : WithBot ℕ∞)) (I : Ideal A)
    (hI : (1 : WithBot ℕ∞) ≤ ringKrullDim (A ⧸ I)) :
    IsAffineOpen (complZeroLocusOpen A I)

Sources

• Section 51.16, Tag 0EB0
• AxiomMath/Stacks at 5ed82d14

LeanStacks.LocalCohomology.cohomologicalDimension_lt_of_le_of_le_jacobson · Stacks.LocalCohomology.cohomologicalDimension_lt_of_isZero_localCohomologyModule · Stacks.LocalCohomology.surjective_smul_top_localCohomologyModule_of_avoidsTopMinimalPrimes · Stacks.LocalCohomology.cohomologicalDimension_lt_of_isZero_homology_localCohomologyDerived · Ideal.exists_symbolicPower_le_pow · Stacks.LocalCohomology.cohomologicalDimension_lt_of_minimalPrimes_adicCompletion · Stacks.LocalCohomology.cohomologicalDimension_lt_of_isExcellent_of_isNormalRing · Stacks.LocalCohomology.isAffineOpen_complZeroLocusOpen_of_isExcellent_of_isNormalRing

Section51.17 Frobenius action#

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

Tag 0EBV, a lemma

Tag 0EBV in the Stacks Project.

free_of_frobenius_baseChange_equiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/FrobeniusAction/FrobeniusBaseChange.lean, line 89.

A finite Frobenius-periodic module over a Noetherian local ring is free.

theorem free_of_frobenius_baseChange_equiv
    {A : Type u} {M : Type v} [CommRing A] [IsLocalRing A] [IsNoetherianRing A]
    [AddCommGroup M] [Module A M] [Module.Finite A M]
    (p : ℕ) [Fact p.Prime] [CharP A p]
    (h : Nonempty (frobeniusBaseChange A p M ≃ₗ[A] M)) :
    Module.Free A M

Tag 0EBW, a lemma

Tag 0EBW in the Stacks Project.

isIdealIndependent_snoc_left_of_mul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/FrobeniusAction/IdealIndependent.lean, line 51.

If an ideal-independent finite family ends in x * y, replacing its last member by x gives another ideal-independent family.

theorem isIdealIndependent_snoc_left_of_mul {A : Type*} [CommRing A] {n : ℕ}
    (f : Fin n → A) (x y : A)
    (h : IsIdealIndependent (Fin.snoc f (x * y))) :
    IsIdealIndependent (Fin.snoc f x)

Tag 0EBX, a lemma

Tag 0EBX in the Stacks Project.

length_quotient_eq_add_of_isIndependent_mul, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/FrobeniusAction/LengthQuotient.lean, line 91.

Stacks Project, Tag 0EBX. If appending f * g to a list gives an independent list, then the length of the quotient by that list is the sum of the lengths of the quotients obtained by appending f and g separately.

lemma length_quotient_eq_add_of_isIndependent_mul (init : List A) (f g : A)
    (h : IsIdealIndependent (fun i : Fin (init ++ [f * g]).length ↦
      (init ++ [f * g])[i])) :
    Module.length A (A ⧸ Ideal.ofList (init ++ [f * g])) =
      Module.length A (A ⧸ Ideal.ofList (init ++ [f])) +
        Module.length A (A ⧸ Ideal.ofList (init ++ [g]))

Tag 0EBY, a lemma

Tag 0EBY in the Stacks Project.

length_quotient_span_powers_eq_prod, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/FrobeniusAction/LengthQuotientPowers.lean, line 220.

Stacks Project, Tag 0EBY. If x generates the maximal ideal of a local ring and the positive powers x i ^ e i are independent, then the quotient by those powers has length equal to the product of the exponents.

lemma length_quotient_span_powers_eq_prod {A : Type*} [CommRing A] [IsLocalRing A]
    {r : ℕ} (x : Fin r → A) (e : Fin r → ℕ)
    (hx : Ideal.span (Set.range x) = IsLocalRing.maximalIdeal A)
    (he : ∀ i, 0 < e i)
    (hind : ∀ (a : Fin r → A), (∑ i, a i * x i ^ e i) = 0 →
      ∀ i, a i ∈ Ideal.span (Set.range fun j ↦ x j ^ e j)) :
    Module.length A (A ⧸ Ideal.span (Set.range fun i ↦ x i ^ e i)) =
      ((∏ i, e i : ℕ) : ℕ∞)

Tag 0EBZ, a lemma

Tag 0EBZ in the Stacks Project.

isIdealIndependent_map_of_flat, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/FrobeniusAction/IdealIndependentFlat.lean, line 51.

The image of an ideal-independent family under a flat ring map is ideal-independent.

lemma isIdealIndependent_map_of_flat
    {A : Type u} {B : Type v} [CommRing A] [CommRing B]
    {ι : Type w} (φ : A →+* B) (hφ : RingHom.Flat φ)
    {f : ι → A} (hf : IsIdealIndependent f) :
    IsIdealIndependent (fun i ↦ φ (f i))

Tag 0EC0, a lemma

Tag 0EC0 in the Stacks Project.

isRegularRing_iff_frobeniusOfPrime_flat, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/FrobeniusAction/Kunz.lean, line 743.

Kunz's theorem. If a prime number vanishes in a Noetherian ring, the ring is regular if and only if its Frobenius endomorphism is flat.

lemma isRegularRing_iff_frobeniusOfPrime_flat {A : Type*} [CommRing A] [IsNoetherianRing A]
    (p : ℕ) (hp : p.Prime) (hchar : (p : A) = 0) :
    IsRegularRing A ↔ RingHom.Flat (frobeniusOfPrime p hp hchar)

Sources

• Section 51.17, Tag 0EBU
• AxiomMath/Stacks at 5ed82d14

Leanfree_of_frobenius_baseChange_equiv · isIdealIndependent_snoc_left_of_mul · length_quotient_eq_add_of_isIndependent_mul · length_quotient_span_powers_eq_prod · isIdealIndependent_map_of_flat · isRegularRing_iff_frobeniusOfPrime_flat

Section51.18 Structure of certain modules#

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

Tag 0EC2, a lemma

Tag 0EC2 in the Stacks Project.

MvPowerSeries.exists_linearEquiv_directSum_injectiveHull_of_leibniz, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/MvPowerSeries/LeibnizTorsionModule.lean, line 703.

A maximal-ideal-power-torsion module over a characteristic-zero formal power series ring, equipped with additive operators satisfying the partial-derivative Leibniz rules, is a direct sum of copies of an injective hull of the residue field.

theorem exists_linearEquiv_directSum_injectiveHull_of_leibniz
    (k : Type u) [Field k] [CharZero k]
    (d : ℕ) (_hd : 0 < d)
    (M : Type v) [AddCommGroup M] [Module (MvPowerSeries (Fin d) k) M]
    (E : Type u) [AddCommGroup E] [Module (MvPowerSeries (Fin d) k) E]
    (i : (ModuleCat.restrictScalars
        (MvPowerSeries.constantCoeff : MvPowerSeries (Fin d) k →+* k)).obj
          (ModuleCat.of k k) ⟶ ModuleCat.of (MvPowerSeries (Fin d) k) E)
    [Mono i]
    (_hi : Module.IsInjectiveHull i)
    (_hM : IsIPowerTorsion (MvPowerSeries (Fin d) k) M
      (IsLocalRing.maximalIdeal (MvPowerSeries (Fin d) k)))
    (D : Fin d → M →+ M)
    (_hD : ∀ (j : Fin d) (f : MvPowerSeries (Fin d) k) (z : M),
      D j (f • z) = MvPowerSeries.pderiv (R := k) j f • z + f • D j z) :
    ∃ J : Type v, Nonempty (M ≃ₗ[MvPowerSeries (Fin d) k] ⨁ _ : J, E)

Tag 0EC3, a lemma

Tag 0EC3 in the Stacks Project.

Dualizing.isIPowerTorsion_frobeniusStable_exists_equiv_directSum_injectiveHull, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Dualizing/FrobeniusStableTorsion.lean, line 620.

Stacks Project, Tag 0EC3. A maximal-ideal-power-torsion module over a regular local ring of prime characteristic which is invariant under extension of scalars by Frobenius is a direct sum of copies of the injective hull of the residue field.

public theorem isIPowerTorsion_frobeniusStable_exists_equiv_directSum_injectiveHull
    (p : ℕ) (hp : p.Prime)
    (A : Type u) [CommRing A] [IsRegularLocalRing A] (hchar : (p : A) = 0)
    (M : Type (max u v)) [AddCommGroup M] [Module A M]
    (hM : IsIPowerTorsion A M (IsLocalRing.maximalIdeal A))
    (hF : (ModuleCat.extendScalars (frobeniusOfPrime p hp hchar)).obj
      (ModuleCat.of A M) ≅ ModuleCat.of A M)
    (E : Type u) [AddCommGroup E] [Module A E]
    (i : ModuleCat.of A (IsLocalRing.ResidueField A) ⟶ ModuleCat.of A E) [Mono i]
    (hi : Module.IsInjectiveHull i) :
    ∃ J : Type (max u v), Nonempty (M ≃ₗ[A] ⨁ _ : J, E)

Sources

• Section 51.18, Tag 0EC1
• AxiomMath/Stacks at 5ed82d14

LeanMvPowerSeries.exists_linearEquiv_directSum_injectiveHull_of_leibniz · Dualizing.isIPowerTorsion_frobeniusStable_exists_equiv_directSum_injectiveHull

Section51.19 Additional structure on local cohomology#

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

Tag 0EC5, a lemma

Tag 0EC5 in the Stacks Project.

Stacks.LocalCohomology.derivationOperator, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/DerivationAction.lean, line 408.

Stacks Project, Tag 0EC5. A derivation θ of A induces a canonical additive operator on each local cohomology module H^i_{V(I)}(A), satisfying the Leibniz rule D (a x) = θ(a) x + a D(x). It is characterized on Čech cohomology classes by the unique extensions of θ to the localizations appearing in the Čech complex, for every finite generating family of I; Stacks.LocalCohomology.DerivationOperator.ext is the uniqueness this characterization provides.

def derivationOperator (A : Type u) [CommRing A] (I : Ideal A) (hI : I.FG)
    (θ : Derivation ℤ A A) (i : ℕ) : DerivationOperator A I hI i θ

Tag 0EC6, a lemma

Tag 0EC6 in the Stacks Project.

Stacks.LocalCohomology.localCohomologyOfRing_frobeniusIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/LocalCohomology/Frobenius.lean, line 134.

Stacks Project, Tag 0EC6. For a commutative ring A in which a prime p vanishes and a finitely generated ideal I, derived extension of scalars along the Frobenius endomorphism fixes the local cohomology RΓ_{V(I)}(A) of the regular module up to isomorphism.

def localCohomologyOfRing_frobeniusIso (A : Type u) [CommRing A] (p : ℕ) (hp : p.Prime)
    (hp0 : (p : A) = 0) (I : Ideal A) (hI : I.FG) :
    (derivedExtensionScalarsGeneral.{u, u, u} (frobeniusOfNatCastEqZero A p hp hp0)).functor.obj
        ((localCohomologyDerived A I hI).obj
          ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj (ModuleCat.of A A))) ≅
      (localCohomologyDerived A I hI).obj
        ((DerivedCategory.singleFunctor (ModuleCat.{u} A) 0).obj (ModuleCat.of A A))

Tag 0EC7, a lemma

Tag 0EC7 in the Stacks Project.

Stacks.EtaleDerivation.subsingleton_sheafDerivation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/StructureSheafDerivation.lean, line 886. The attribute's comment: “uniqueness”.

The affine-normalized, restriction-compatible extension of a base derivation to the structure sheaf is unique.

theorem subsingleton_sheafDerivation {A : Type u} [CommRing A] {V : Scheme.{u}}
    (f : V ⟶ Spec (.of A)) (θ : Derivation ℤ A A) :
    Subsingleton (SheafDerivation f θ)

Stacks.EtaleDerivation.nonempty_twistedDerivation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/StructureSheafDerivation.lean, line 911. The attribute's comment: “existence and Leibniz rule”.

An absolute derivation of the base ring extends to an affine-normalized derivation of the structure sheaf of a quasi-compact, quasi-separated étale scheme. In every degree its induced additive operator on the canonical cohomology module satisfies the twisted Leibniz rule.

theorem nonempty_twistedDerivation {A : Type u} [CommRing A] {V : Scheme.{u}}
    (f : V ⟶ Spec (.of A)) [QuasiCompact f] [QuasiSeparated f] [Etale f]
    (θ : Derivation ℤ A A) (i : ℕ) : Nonempty (TwistedDerivation f i θ)

Tag 0EC9, a lemma

Tag 0EC9 in the Stacks Project.

Stacks.EtaleFrobenius.nonempty_extendScalarsDerived_derivedGlobalSections_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FrobeniusBaseChange.lean, line 230. The attribute's comment: “cohomology and base change is the explicit hypothesis Stacks.EtaleFrobenius.DerivedGlobalSectionsBaseChange A, namely Stacks 08IB for the structure sheaf over an affine base: for every ring map out of A and every Cartesian square over its spectrum whose left-hand morphism is flat, quasi-compact and quasi-separated, derived extension of scalars carries the derived global sections of the source to those of the base change. The library carries the base change morphism of Stacks 08HY but not its invertibility in Tor-independent generality, whose globalization step is Stacks 0DJ9. Everything else is proved: the Cartesian square supplied to that hypothesis is the absolute Frobenius square of V, Cartesian by Stacks 0EBS”.

Let p be a prime number, let A be a commutative ring in which p vanishes and let F : A → A, a ↦ aᵖ, be its Frobenius endomorphism. Assuming cohomology and base change Stacks.EtaleFrobenius.DerivedGlobalSectionsBaseChange A, for a quasi-compact, quasi-separated, étale scheme V over Spec A there is an isomorphism

RΓ(V, 𝒪_V) ⊗^L_{A, F} A ≅ RΓ(V, 𝒪_V)

in D(A).

theorem nonempty_extendScalarsDerived_derivedGlobalSections_iso
    [QuasiCompact f] [QuasiSeparated f] [Etale f]
    (hbc : DerivedGlobalSectionsBaseChange A) :
    Nonempty ((StacksDraft.PseudoCoherence.extendScalarsDerived
        (Stacks.LocalCohomology.frobeniusOfNatCastEqZero A p Fact.out hp0)).obj
        ((derivedGlobalSectionsOver f).obj (derivedStructureSheaf V)) ≅
      (derivedGlobalSectionsOver f).obj (derivedStructureSheaf V))

Stacks.EtaleFrobenius.nonempty_extendScalarsDerived_derivedGlobalSections_iso_of_etale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/FrobeniusCohomologyBaseChange.lean, line 79.

Stacks Project, Tag 0EC9. Let p be a prime number, let A be a commutative ring in which p vanishes and let F : A → A, a ↦ aᵖ, be its Frobenius endomorphism. If V ⟶ Spec A is quasi-compact, quasi-separated and étale, then there exists an isomorphism

RΓ(V, 𝒪_V) ⊗^L_{A, F} A ≅ RΓ(V, 𝒪_V)

in D(A).

The relative Frobenius of V is an isomorphism ([Stacks, Tag 0EBS]), so the absolute Frobenius square of V is cartesian, and cohomology and base change for the flat morphism V ⟶ Spec A (derivedGlobalSectionsBaseChange, [Stacks, Tag 08IB]) applies to it.

theorem nonempty_extendScalarsDerived_derivedGlobalSections_iso_of_etale
    [QuasiCompact f] [QuasiSeparated f] [Etale f] :
    Nonempty ((StacksDraft.PseudoCoherence.extendScalarsDerived
        (Stacks.LocalCohomology.frobeniusOfNatCastEqZero A p Fact.out hp0)).obj
        ((derivedGlobalSectionsOver f).obj (derivedStructureSheaf V)) ≅
      (derivedGlobalSectionsOver f).obj (derivedStructureSheaf V))

Sources

• Section 51.19, Tag 0EC4
• AxiomMath/Stacks at 5ed82d14

LeanStacks.LocalCohomology.derivationOperator · Stacks.LocalCohomology.localCohomologyOfRing_frobeniusIso · Stacks.EtaleDerivation.subsingleton_sheafDerivation · Stacks.EtaleDerivation.nonempty_twistedDerivation · Stacks.EtaleFrobenius.nonempty_extendScalarsDerived_derivedGlobalSections_iso · Stacks.EtaleFrobenius.nonempty_extendScalarsDerived_derivedGlobalSections_iso_of_etale

Section51.20 A bit of uniformity, I#

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

Tag 0G9T, a lemma

Tag 0G9T in the Stacks Project.

factor_through_free_of_tor_one_map_eq_zero, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityI/FactorThroughFree.lean, line 300.

Stacks Project, Tag 0G9T. A map from a finitely presented module which induces the zero map on Tor₁ with every module factors through a free module.

lemma factor_through_free_of_tor_one_map_eq_zero
    {R : Type u} [CommRing R] {M M' : ModuleCat.{u} R} (f : M ⟶ M')
    [Module.FinitePresentation R M]
    (hf : ∀ N : ModuleCat.{u} R,
      ((Tor' (ModuleCat.{u} R) 1).map f).app N = 0) :
    FactorsThroughFree f.hom

Tag 0G9U, an equation

Tag 0G9U in the Stacks Project.

CategoryTheory.exists_shortExact_pushout, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/Support/ShortExactPushout.lean, line 38.

The pushout of the left-hand map in a short exact sequence is again a short exact sequence, with the same right-hand object.

theorem exists_shortExact_pushout
    {C : Type u} [Category C] [Abelian C]
    {K P M K' : C} {i : K ⟶ P} {p : P ⟶ M}
    (hip : i ≫ p = 0) (h : (ShortComplex.mk i p hip).ShortExact) (a : K ⟶ K') :
    ∃ (E : C) (j : P ⟶ E) (i' : K' ⟶ E) (q : E ⟶ M)
      (hi'q : i' ≫ q = 0),
      IsPushout i a j i' ∧ j ≫ q = p ∧ (ShortComplex.mk i' q hi'q).ShortExact

Tag 0G9V, a lemma

Tag 0G9V in the Stacks Project.

tfae_lift_ext_conditions, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityI/VanishingEquivalences.lean, line 415. The attribute's comment: “equivalence of conditions (1)--(5)”.

Conditions (1)--(5) are equivalent.

lemma tfae_lift_ext_conditions :
    List.TFAE [
      HasLiftVanishingAbove p p' alpha e,
      HasLiftVanishingAtSucc p p' alpha e,
      ExtMapVanishesAbove alpha e,
      ExtMapVanishesAtSucc alpha e,
      CanonicalExtClassPullbackVanishes p p' alpha e]

canonicalExtClassPullbackVanishes_imp_torMapVanishesAbove, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityI/VanishingEquivalences.lean, line 508. The attribute's comment: “condition (5) implies condition (6)”.

Condition (5) implies condition (6).

lemma canonicalExtClassPullbackVanishes_imp_torMapVanishesAbove :
    CanonicalExtClassPullbackVanishes p p' alpha e → TorMapVanishesAbove alpha e

tfae_tor_conditions, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityI/VanishingEquivalences.lean, line 515. The attribute's comment: “equivalence of conditions (6) and (7)”.

Conditions (6) and (7) are equivalent.

lemma tfae_tor_conditions :
    List.TFAE [TorMapVanishesAbove alpha e, TorMapVanishesAtSucc alpha e]

tfae_of_isPseudoCoherentFrom, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityI/VanishingEquivalences.lean, line 685. The attribute's comment: “all conditions under pseudo-coherence”.

If M is (-e-1)-pseudo-coherent, all seven conditions are equivalent.

lemma tfae_of_isPseudoCoherentFrom
    (hM : StacksDraft.PseudoCoherence.IsPseudoCoherentFrom
      ((DerivedCategory.singleFunctor (ModuleCat.{u} R) 0).obj M) (-(e : ℤ) - 1)) :
    List.TFAE [
      HasLiftVanishingAbove p p' alpha e,
      HasLiftVanishingAtSucc p p' alpha e,
      ExtMapVanishesAbove alpha e,
      ExtMapVanishesAtSucc alpha e,
      CanonicalExtClassPullbackVanishes p p' alpha e,
      TorMapVanishesAbove alpha e,
      TorMapVanishesAtSucc alpha e]

tfae_of_isNoetherianRing_of_finite, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityI/VanishingEquivalences.lean, line 709. The attribute's comment: “Noetherian finite-module case”.

Over a Noetherian ring, all seven conditions are equivalent when M is finite.

lemma tfae_of_isNoetherianRing_of_finite [IsNoetherianRing R] [Module.Finite R M] :
    List.TFAE [
      HasLiftVanishingAbove p p' alpha e,
      HasLiftVanishingAtSucc p p' alpha e,
      ExtMapVanishesAbove alpha e,
      ExtMapVanishesAtSucc alpha e,
      CanonicalExtClassPullbackVanishes p p' alpha e,
      TorMapVanishesAbove alpha e,
      TorMapVanishesAtSucc alpha e]

Tag 0EH1, a lemma

Tag 0EH1 in the Stacks Project.

Stacks.LocalCohomology.exists_quotientPower_extMapVanishesAbove, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityI/QuotientPowerVanishing.lean, line 212.

[Stacks, Tag 0EH1]. Let I be an ideal of a Noetherian ring A and let e be the cohomological dimension of I in A. For every n there is an m > n for which the quotient map A/I^m → A/I^n satisfies the equivalent conditions of [Stacks, Tag 0G9V] in degree e: Ext^i(A/I^n, N) → Ext^i(A/I^m, N) is zero for every A-module N and every i > e.

theorem exists_quotientPower_extMapVanishesAbove
    (A : Type u) [CommRing A] [IsNoetherianRing A] (I : Ideal A) (n : ℕ) :
    ∃ m : ℕ, ∃ hnm : n < m,
      ExtMapVanishesAbove
        (ModuleCat.ofHom (Ideal.Quotient.factorₐ A
          (Ideal.pow_le_pow_right (I := I) (Nat.le_of_lt hnm))).toLinearMap)
        (cohomologicalDimension A I (IsNoetherian.noetherian I)).toNat

Sources

• Section 51.20, Tag 0G9S
• AxiomMath/Stacks at 5ed82d14

Leanfactor_through_free_of_tor_one_map_eq_zero · CategoryTheory.exists_shortExact_pushout · tfae_lift_ext_conditions · canonicalExtClassPullbackVanishes_imp_torMapVanishesAbove · tfae_tor_conditions · tfae_of_isPseudoCoherentFrom · tfae_of_isNoetherianRing_of_finite · Stacks.LocalCohomology.exists_quotientPower_extMapVanishesAbove

Section51.21 A bit of uniformity, II#

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

Tag 0G9X, a lemma

Tag 0G9X in the Stacks Project.

exists_uniform_tor_transition_eq_zero_of_pow_smul_eq_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityII/UniformTorTransition.lean, line 816.

Stacks Project, Tag 0G9X. For a fixed power I ^ m and a positive Tor degree, there is a uniform shift such that the transition from A / I ^ n to A / I ^ (n - c) induces the zero map on Tor against every module annihilated by I ^ m.

theorem exists_uniform_tor_transition_eq_zero_of_pow_smul_eq_bot
    {A : Type u} [CommRing A] [IsNoetherianRing A] (I : Ideal A) (m i : ℕ) (hi : 0 < i) :
    ∃ c : ℕ, ∀ (M : ModuleCat.{u} A),
      I ^ m • (⊤ : Submodule A M) = ⊥ → ∀ n : ℕ, c ≤ n →
        ((Tor (ModuleCat.{u} A) i).obj M).map
          (ModuleCat.ofHom (Submodule.factor (p := I ^ n) (p' := I ^ (n - c))
            (Ideal.pow_le_pow_right (Nat.sub_le n c)))) = 0

Tag 0G9Y, a lemma

Tag 0G9Y in the Stacks Project.

Stacks.Blowup.exists_pow_le_annihilator_tor_affineBlowupAlgebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Blowup/TorAnnihilation.lean, line 485.

Uniform annihilation of the high Tor modules of an affine blowup algebra. Let I = (a₁, …, a_t) be an ideal of a Noetherian ring A, let a = a₁, and let B = A[I/a] be the affine blowup algebra. There is a c > 0 such that Iᶜ annihilates Torᴬᵢ(B, M) for every A-module M and every i ≥ t.

public theorem exists_pow_le_annihilator_tor_affineBlowupAlgebra
    {A : Type u} [CommRing A] [IsNoetherianRing A] {n : ℕ} (g : Fin (n + 1) → A)
    (I : Ideal A) (hI : I = Ideal.span (Set.range g))
    (S : Type u) [CommRing S] [Algebra A S] [IsLocalization.Away (g 0) S] :
    ∃ c : ℕ, 0 < c ∧ ∀ (M : ModuleCat.{u} A) (i : ℕ), n + 1 ≤ i →
      I ^ c ≤ Module.annihilator A
        (((Tor (ModuleCat.{u} A) i).obj
          (ModuleCat.of A ↥(affineBlowupAlgebra I (g 0) S))).obj M)

Tag 0G9Z, a lemma

Tag 0G9Z in the Stacks Project.

Stacks.Blowup.exists_threshold_nonempty_derivedGlobalSectionsTwistedPullback_iso_derivedTensorIdealPow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/TwistedSectionsIdealPow.lean, line 168.

Cohomology of the twisted derived pullback along the affine blowup, unconditionally. Let A be a Noetherian ring, I ⊆ A an ideal and p : X ⟶ Spec A the blowup of Spec A in I. There is a q₀ such that for every n ≥ q₀ and any A-module M,

RΓ(X, Lp^*(M̃) ⊗^𝐋_{𝒪_X} 𝒪_X(n)) ≅ M ⊗^𝐋_A Iⁿ in D(A).

theorem exists_threshold_nonempty_derivedGlobalSectionsTwistedPullback_iso_derivedTensorIdealPow
    [IsNoetherianRing A] :
    ∃ q₀ : ℕ, ∀ n : ℕ, q₀ ≤ n →
      ∀ M : ModuleCat.{u} (CommRingCat.of A),
        Nonempty ((AlgebraicGeometry.derivedGlobalSectionsOver (toSpec I)).obj
            (((Stacks.Cohomology.TorAmplitude.derTensor (blowUpRingedSpace I)).tensor.obj
                ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
                  (toSpecRingedSpace I)).obj (DerivedCategory.Q.obj (tildeComplex
                    ((CochainComplex.singleFunctor (ModuleCat.{u} (CommRingCat.of A)) 0).obj
                      M))))).obj
              (DerivedCategory.Q.obj
                ((CochainComplex.singleFunctor (BlowUpModules I) 0).obj
                  (blowUpTwist I (n : ℤ))))) ≅
          ((CochainComplex.DerivedTensor.canonicalDerivedTensorProduct A).tensor.obj
              (DerivedCategory.Q.obj
                ((CochainComplex.singleFunctor (ModuleCat.{u} A) 0).obj M))).obj
            (DerivedCategory.Q.obj
              ((CochainComplex.singleFunctor (ModuleCat.{u} A) 0).obj
                (ModuleCat.of A (I ^ n : Ideal A)))))

Tag 0GA0, a lemma

Tag 0GA0 in the Stacks Project.

Stacks.Blowup.exists_pow_le_annihilator_homology_derivedPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/DerivedPullbackAnnihilation.lean, line 505.

Stacks Project, Tag 0GA0. Let A be a Noetherian ring and I = (a₀, …, a_n) ⊆ A an ideal with t = n + 1 generators, and let p : X ⟶ Spec A be the blowup of Spec A in I, that is X = Proj(⨁_{m ≥ 0} Iᵐ). There is an integer c > 0, depending only on A and I, such that for every A-module M the cohomology sheaves H^j(Lp^*M̃) are annihilated by Iᶜ for all j ≤ -t.

Annihilation is expressed on sections: an element r ∈ Iᶜ, viewed as a global section of X through p and restricted to an open U, kills every section of H^j(Lp^*M̃) over U.

theorem exists_pow_le_annihilator_homology_derivedPullback {n : ℕ} (g : Fin (n + 1) → A)
    (I : Ideal A) (hI : I = Ideal.span (Set.range g)) :
    ∃ c : ℕ, 0 < c ∧ ∀ (M : ModuleCat.{u} (CommRingCat.of A)) (j : ℤ), j ≤ -((n : ℤ) + 1) →
      ∀ (U : (blowUpSpec I).Opens) (r : A), r ∈ I ^ c →
        ∀ s : Γ((DerivedCategory.homologyFunctor (blowUpSpec I).Modules j).obj
            ((Stacks.Cohomology.DerivedAdjunctionOnRingedSpaces.derivedPullback
              (toSpecRingedSpace I)).obj (DerivedCategory.Q.obj (tildeComplex
              ((CochainComplex.singleFunctor (ModuleCat.{u} (CommRingCat.of A)) 0).obj M)))), U),
          (blowUpSpec I).presheaf.map (homOfLE (show U ≤ ⊤ from le_top)).op
            ((toSpec I).appTop ((Scheme.ΓSpecIso (CommRingCat.of A)).inv r)) • s = 0

Tag 0GA1, a lemma

Tag 0GA1 in the Stacks Project.

Stacks.LocalCohomology.UniformityII.exists_pow_le_annihilator_tor_quotient_pow_blowup, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityII/TorAnnihilationBlowup.lean, line 211.

Stacks Project, Tag 0GA1. Let A be a Noetherian ring and let I = (g 0, …, g (t-1)) be an ideal of A generated by at most t elements, as in the Situation of [Stacks, Tag 0G9W]. There is an integer m, depending only on A and I, such that for every A-module M the modules Tor_i^A(M, A/I^q) are annihilated by I^m for all i > t and all q ≥ 0.

Nothing is assumed. The spectral sequence the source's proof runs on is produced by Stacks.Blowup.exists_hypercohomologySpectralSequence_abutsTo_tor_idealPow on the blowup of Spec A in I, and the step from it to the filtration of Tor_i^A(M, Iᑫ) that Stacks.LocalCohomology.UniformityII.exists_pow_le_annihilator_tor_quotient_pow asks for is Stacks.LocalCohomology.UniformityII .exists_pow_le_annihilator_tor_quotient_pow_of_abutsTo_restrictScalars.

theorem exists_pow_le_annihilator_tor_quotient_pow_blowup [IsNoetherianRing A] {I : Ideal A}
    {t : ℕ} (g : Fin t → A) (hg : I = Ideal.span (Set.range g)) :
    ∃ m : ℕ, ∀ (M : ModuleCat.{u} A) (i q : ℕ), t < i →
      I ^ m ≤ Module.annihilator A
        (((Tor' (ModuleCat.{u} A) i).obj M).obj (ModuleCat.of A (A ⧸ I ^ q)))

Stacks.LocalCohomology.UniformityII.exists_pow_le_annihilator_tor_quotient_pow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityII/UniformTorAnnihilation.lean, line 208.

Stacks Project, Tag 0GA1. Let A be a Noetherian ring and let I = (g 0, …, g (t-1)) be an ideal of A generated by at most t elements, as in the Situation of [Stacks, Tag 0G9W]. There is an integer m, depending only on A and I, such that for every A-module M the modules Tor_i^A(M, A/I^q) are annihilated by I^m for all i > t and all q ≥ 0.

The hypothesis hfilt is the geometric input of the source's proof, which is not formalized here: for all i ≥ t and all q ≥ q₀, the module Tor_i^A(M, I^q) carries a filtration ⊤ = F 0, …, F d = ⊥ in d steps whose graded pieces are annihilated by Iᶜ. The source produces it from the hypercohomology spectral sequence [Stacks, Tag 0G9Q] of Lp^*M̃(q) on the blowup p : X ⟶ Spec A of Spec A in I, with q₀ = q(A, I), with d = t by the vanishing [Stacks, Tag 071L] for the cover of X by the t affine charts, and with c = c(A, I) the exponent of [Stacks, Tag 0GA0]; the identification of the abutment with Tor_i^A(M, I^q) is [Stacks, Tag 0G9Z].

Given hfilt, the exponent m = max (d * c) q₀ + 1 works: above the threshold the filtration gives I^{dc} • Tor_i^A(M, I^q) = 0 for i ≥ t, which the sequence 0 → I^q → A → A/I^q → 0 shifts to A/I^q for i > t, and for the remaining q ≤ m already I^m ≤ I^q annihilates A/I^q and hence Tor_i^A(M, A/I^q).

theorem exists_pow_le_annihilator_tor_quotient_pow [IsNoetherianRing A] {I : Ideal A} {t : ℕ}
    (g : Fin t → A) (hg : I = Ideal.span (Set.range g)) (q₀ d c : ℕ)
    (hfilt : ∀ (M : ModuleCat.{u} A) (i q : ℕ), t ≤ i → q₀ ≤ q →
      ∃ F : ℕ → Submodule A
          (((Tor' (ModuleCat.{u} A) i).obj M).obj (ModuleCat.of A ↥(I ^ q))),
        F 0 = ⊤ ∧ F d = ⊥ ∧ ∀ k, I ^ c • F k ≤ F (k + 1)) :
    ∃ m : ℕ, ∀ (M : ModuleCat.{u} A) (i q : ℕ), t < i →
      I ^ m ≤ Module.annihilator A
        (((Tor' (ModuleCat.{u} A) i).obj M).obj (ModuleCat.of A (A ⧸ I ^ q)))

Stacks.LocalCohomology.UniformityII.exists_pow_le_annihilator_tor_quotient_pow_of_card_le_one, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityII/UniformTorAnnihilation.lean, line 295. The attribute's comment: “for an ideal generated by at most one element”.

Stacks Project, Tag 0GA1 for an ideal generated by at most one element. Let A be a Noetherian ring and let I = (g 0, …, g (t-1)) be an ideal generated by at most t ≤ 1 elements. There is an integer m, depending only on A and I, such that for every A-module M the modules Tor_i^A(M, A/I^q) are annihilated by I^m for all i > t and all q ≥ 0. Nothing is assumed: the geometric input of exists_pow_le_annihilator_tor_quotient_pow is not needed here.

For t = 1 and I = (a) take m = q₀, an index at which the ascending chain of annihilators ann(a) ⊆ ann(a²) ⊆ ⋯ stabilizes. For q ≤ q₀ already I^{q₀} ≤ I^q annihilates A/I^q. For q > q₀ the ideal I^q = (a^q) is the cyclic module A ⧸ ann(a^q) with ann(a^q) = ann(a^{q₀}) annihilated by a^{q₀}, so one dimension shift gives a^{q₀} · Tor_i^A(M, I^q) = 0 for i ≥ 1 and a second, along 0 → I^q → A → A/I^q → 0, gives the claim for i > 1. The case t = 0, where I = 0, is the degenerate case of exists_pow_le_annihilator_tor_quotient_pow.

theorem exists_pow_le_annihilator_tor_quotient_pow_of_card_le_one [IsNoetherianRing A]
    {I : Ideal A} {t : ℕ} (g : Fin t → A) (hg : I = Ideal.span (Set.range g)) (ht : t ≤ 1) :
    ∃ m : ℕ, ∀ (M : ModuleCat.{u} A) (i q : ℕ), t < i →
      I ^ m ≤ Module.annihilator A
        (((Tor' (ModuleCat.{u} A) i).obj M).obj (ModuleCat.of A (A ⧸ I ^ q)))

Tag 0GA2, a lemma

Tag 0GA2 in the Stacks Project.

exists_uniform_tor_transition_eq_zero_of_pow_le_annihilator_tor', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityII/UniformTorTransition.lean, line 1227.

Stacks Project, Tag 0GA2. Let I = (g 0, …, g (t - 1)) be an ideal of a Noetherian ring A generated by at most t elements. There are N and c, depending only on A, I and t, such that the surjection A / I ^ n ↠ A / I ^ (n - c) induces the zero map Tor_{t+1}^A(M, A/I^n) → Tor_{t+1}^A(M, A/I^{n-c}) for every A-module M and every n ≥ N. That N and c are produced before the module is seen is the whole content of the source's lemma.

The power I ^ c₁ annihilating Tor_i^A(M, A/I^q) for all M, all i > t and all q, which the source's induction starts from, is [Stacks, Tag 0GA1], Stacks.LocalCohomology.UniformityII.exists_pow_le_annihilator_tor_quotient_pow_blowup.

theorem exists_uniform_tor_transition_eq_zero_of_pow_le_annihilator_tor'
    {A : Type u} [CommRing A] [IsNoetherianRing A] {I : Ideal A} {t : ℕ}
    (g : Fin t → A) (hg : I = Ideal.span (Set.range g)) :
    ∃ N c : ℕ, ∀ (M : ModuleCat.{u} A) (n : ℕ), N ≤ n →
      ((Tor (ModuleCat.{u} A) (t + 1)).obj M).map
        (ModuleCat.ofHom (Submodule.factor (p := I ^ n) (p' := I ^ (n - c))
          (Ideal.pow_le_pow_right (Nat.sub_le n c)))) = 0

Tag 0GA3, a proposition

Tag 0GA3 in the Stacks Project.

Stacks.LocalCohomology.UniformityII.exists_uniform_torMapVanishesAtSucc_quotientFactor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityII/UniformVanishingConditions.lean, line 142. The attribute's comment: “condition (7) of Tag 0G9V”.

Stacks Project, Tag 0GA3, condition (7) of Tag 0G9V. Let I = (g 0, …, g (t - 1)) be an ideal of a Noetherian ring A generated by at most t elements. There are N and c, depending only on A, I and t, such that for every n ≥ N the transition A / I ^ n ↠ A / I ^ (n - c) induces the zero map on Tor _ (t + 1) against every module.

This is [Stacks, Tag 0GA2], exists_uniform_tor_transition_eq_zero_of_pow_le_annihilator_tor', read through the braiding of the two models of Tor.

theorem exists_uniform_torMapVanishesAtSucc_quotientFactor [IsNoetherianRing A]
    {I : Ideal A} {t : ℕ} (g : Fin t → A) (hg : I = Ideal.span (Set.range g)) :
    ∃ N c : ℕ, ∀ n : ℕ, N ≤ n →
      TorMapVanishesAtSucc
        (ModuleCat.ofHom (Submodule.factor (p := I ^ n) (p' := I ^ (n - c))
          (Ideal.pow_le_pow_right (Nat.sub_le n c)))) t

Stacks.LocalCohomology.UniformityII.exists_uniform_extMapVanishesAbove_quotientFactor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityII/UniformVanishingConditions.lean, line 162. The attribute's comment: “condition (3) of Tag 0G9V”.

Stacks Project, Tag 0GA3, condition (3) of Tag 0G9V. Let I = (g 0, …, g (t - 1)) be an ideal of a Noetherian ring A generated by at most t elements. There are N and c, depending only on A, I and t, such that for every n ≥ N the transition A / I ^ n ↠ A / I ^ (n - c) induces the zero map Ext ^ i (A / I ^ (n - c), M) → Ext ^ i (A / I ^ n, M) for every module M and every i > t.

As A is Noetherian and A / I ^ n is a finite A-module, all seven conditions of [Stacks, Tag 0G9V] are equivalent for the transition (tfae_of_isNoetherianRing_of_finite), so this is the assertion that the transition satisfies them; it is obtained from condition (7), exists_uniform_torMapVanishesAtSucc_quotientFactor.

theorem exists_uniform_extMapVanishesAbove_quotientFactor [IsNoetherianRing A]
    {I : Ideal A} {t : ℕ} (g : Fin t → A) (hg : I = Ideal.span (Set.range g)) :
    ∃ N c : ℕ, ∀ n : ℕ, N ≤ n →
      ExtMapVanishesAbove
        (ModuleCat.ofHom (Submodule.factor (p := I ^ n) (p' := I ^ (n - c))
          (Ideal.pow_le_pow_right (Nat.sub_le n c)))) t

Stacks.LocalCohomology.UniformityII.exists_uniform_hasLiftVanishingAbove_quotientFactor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityII/UniformVanishingConditions.lean, line 181. The attribute's comment: “condition (1) of Tag 0G9V”.

Stacks Project, Tag 0GA3, condition (1) of Tag 0G9V. Let I = (g 0, …, g (t - 1)) be an ideal of a Noetherian ring A generated by at most t elements. There are N and c, depending only on A, I and t, such that for every n ≥ N and every choice of projective resolutions of A / I ^ n and of A / I ^ (n - c), the transition A / I ^ n ↠ A / I ^ (n - c) lifts to a map of resolutions whose components vanish in all homological degrees above t.

It is obtained from condition (7), exists_uniform_torMapVanishesAtSucc_quotientFactor, by the equivalence of the conditions of [Stacks, Tag 0G9V] for a finite module over a Noetherian ring, tfae_of_isNoetherianRing_of_finite.

theorem exists_uniform_hasLiftVanishingAbove_quotientFactor [IsNoetherianRing A]
    {I : Ideal A} {t : ℕ} (g : Fin t → A) (hg : I = Ideal.span (Set.range g)) :
    ∃ N c : ℕ, ∀ n : ℕ, N ≤ n →
      ∀ {P P' : CochainComplex (ModuleCat.{u} A) ℤ}
        (p : P ⟶ singleComplex (ModuleCat.of A (A ⧸ I ^ n)))
        (p' : P' ⟶ singleComplex (ModuleCat.of A (A ⧸ I ^ (n - c))))
        [CochainComplex.IsProjectiveResolution p]
        [CochainComplex.IsProjectiveResolution p'],
        HasLiftVanishingAbove p p'
          (ModuleCat.ofHom (Submodule.factor (p := I ^ n) (p' := I ^ (n - c))
            (Ideal.pow_le_pow_right (Nat.sub_le n c)))) t

Stacks.LocalCohomology.UniformityII.exists_uniform_vanishingConditions_quotientFactor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityII/UniformVanishingConditions.lean, line 208. The attribute's comment: “all seven conditions of Tag 0G9V at e = t”.

Stacks Project, Tag 0GA3. Let I = (g 0, …, g (t - 1)) be an ideal of a Noetherian ring A generated by at most t elements. There are N and c, depending only on A, I and t, such that for every n ≥ N and every choice of projective resolutions of A / I ^ n and of A / I ^ (n - c), the transition A / I ^ n ↠ A / I ^ (n - c) satisfies all seven conditions of [Stacks, Tag 0G9V] with e = t, in the order of the source: (1) a lift vanishing in all degrees above t, (2) a lift vanishing in degree t + 1, (3) the zero map on Ext ^ i for all i > t, (4) the zero map on Ext ^ (t + 1), (5) the canonical class of degree t + 1 pulls back to zero, (6) the zero map on Tor _ i for all i > t, (7) the zero map on Tor _ (t + 1).

All seven follow from condition (7), exists_uniform_torMapVanishesAtSucc_quotientFactor, by tfae_of_isNoetherianRing_of_finite.

theorem exists_uniform_vanishingConditions_quotientFactor [IsNoetherianRing A]
    {I : Ideal A} {t : ℕ} (g : Fin t → A) (hg : I = Ideal.span (Set.range g)) :
    ∃ N c : ℕ, ∀ n : ℕ, N ≤ n →
      ∀ {P P' : CochainComplex (ModuleCat.{u} A) ℤ}
        (p : P ⟶ singleComplex (ModuleCat.of A (A ⧸ I ^ n)))
        (p' : P' ⟶ singleComplex (ModuleCat.of A (A ⧸ I ^ (n - c))))
        [CochainComplex.IsProjectiveResolution p]
        [CochainComplex.IsProjectiveResolution p'],
        let α := ModuleCat.ofHom (Submodule.factor (p := I ^ n) (p' := I ^ (n - c))
          (Ideal.pow_le_pow_right (Nat.sub_le n c)))
        HasLiftVanishingAbove p p' α t ∧ HasLiftVanishingAtSucc p p' α t ∧
          ExtMapVanishesAbove α t ∧ ExtMapVanishesAtSucc α t ∧
          CanonicalExtClassPullbackVanishes p p' α t ∧ TorMapVanishesAbove α t ∧
          TorMapVanishesAtSucc α t

Tag 0GA4, a remark

Tag 0GA4 in the Stacks Project.

Stacks.LocalCohomology.UniformityII.exists_uniform_vanishingConditions_quotientFactor_of_ringKrullDim, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityII/UniformVanishingKrullDimension.lean, line 142. The attribute's comment: “Tag 0GA3 with e = dim A for a local ring: all seven conditions of Tag 0G9V; the cd(A, I) question the remark raises is open in the source and is not stated”.

Stacks Project, Tag 0GA4. Let A be a Noetherian local ring of Krull dimension d and let I be an ideal of A. There are N and c such that for every n ≥ N and every choice of projective resolutions of A / I ^ n and of A / I ^ (n - c), the transition A / I ^ n ↠ A / I ^ (n - c) satisfies all seven conditions of [Stacks, Tag 0G9V] with e = d, in the order of the source: (1) a lift vanishing in all degrees above d, (2) a lift vanishing in degree d + 1, (3) the zero map on Ext ^ i for all i > d, (4) the zero map on Ext ^ (d + 1), (5) the canonical class of degree d + 1 pulls back to zero, (6) the zero map on Tor _ i for all i > d, (7) the zero map on Tor _ (d + 1).

This is the conclusion of [Stacks, Tag 0GA3] with e = t replaced by e = dim A; no bound on the number of generators of I enters the statement. All seven conditions follow from condition (7), exists_uniform_torMapVanishesAtSucc_quotientFactor_of_ringKrullDim, by tfae_of_isNoetherianRing_of_finite.

theorem exists_uniform_vanishingConditions_quotientFactor_of_ringKrullDim
    [IsNoetherianRing A] [IsLocalRing A] (I : Ideal A) (d : ℕ) (hdim : ringKrullDim A = d) :
    ∃ N c : ℕ, ∀ n : ℕ, N ≤ n →
      ∀ {P P' : CochainComplex (ModuleCat.{u} A) ℤ}
        (p : P ⟶ singleComplex (ModuleCat.of A (A ⧸ I ^ n)))
        (p' : P' ⟶ singleComplex (ModuleCat.of A (A ⧸ I ^ (n - c))))
        [CochainComplex.IsProjectiveResolution p]
        [CochainComplex.IsProjectiveResolution p'],
        let α := ModuleCat.ofHom (Submodule.factor (p := I ^ n) (p' := I ^ (n - c))
          (Ideal.pow_le_pow_right (Nat.sub_le n c)))
        HasLiftVanishingAbove p p' α d ∧ HasLiftVanishingAtSucc p p' α d ∧
          ExtMapVanishesAbove α d ∧ ExtMapVanishesAtSucc α d ∧
          CanonicalExtClassPullbackVanishes p p' α d ∧ TorMapVanishesAbove α d ∧
          TorMapVanishesAtSucc α d

Tag 0GA5, a remark

Tag 0GA5 in the Stacks Project.

Stacks.LocalCohomology.UniformityII.nonempty_strictProIso_systemFour_systemOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityII/NoetherianSystemFour.lean, line 119. The attribute's comment: “if P is Noetherian, the system (4) is strictly pro-isomorphic to the system (1)”.

If P is Noetherian, the system (4) is strictly pro-isomorphic to the system (1). Let φ : P → A be a ring map of Noetherian rings, J ⊆ P an ideal, I = JA, and M a bounded complex of finite A-modules. Then the inverse system n ↦ M ⊗ᴸ_P P/Jⁿ⁺¹ in D(A) is isomorphic, in the strict pro-category of D(A), to the system n ↦ M/Iⁿ⁺¹M. An isomorphism of the strict pro-category is in particular an isomorphism of pro-objects.

theorem nonempty_strictProIso_systemFour_systemOne [IsNoetherianRing P] [IsNoetherianRing A]
    (J : Ideal P) (I : Ideal A) (hI : I = J.map φ)
    (hMbounded : ∃ a b : ℤ, M.IsStrictlyGE a ∧ M.IsStrictlyLE b)
    (hMfinite : ∀ i : ℤ, Module.Finite A (M.X i)) :
    Nonempty (proObj (systemFour φ M J) ≅
      proObj (Stacks.AdicSystem.DerivedReductionProIso.reductionComplexSystem I M ⋙
        DerivedCategory.Q))

Stacks.LocalCohomology.UniformityII.nonempty_proIso_systemFour_systemOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityII/NoetherianSystemFour.lean, line 136. The attribute's comment: “if P is Noetherian, the system (4) is pro-isomorphic to the system (1)”.

If P is Noetherian, the system (4) is pro-isomorphic to the system (1). Let φ : P → A be a ring map of Noetherian rings, J ⊆ P an ideal, I = JA, and M a bounded complex of finite A-modules. Then the inverse systems n ↦ M ⊗ᴸ_P P/Jⁿ⁺¹ and n ↦ M/Iⁿ⁺¹M in D(A) are pro-isomorphic.

theorem nonempty_proIso_systemFour_systemOne [IsNoetherianRing P] [IsNoetherianRing A]
    (J : Ideal P) (I : Ideal A) (hI : I = J.map φ)
    (hMbounded : ∃ a b : ℤ, M.IsStrictlyGE a ∧ M.IsStrictlyLE b)
    (hMfinite : ∀ i : ℤ, Module.Finite A (M.X i)) :
    Nonempty (_root_.InverseSequence.ProIso (systemFour φ M J)
      (Stacks.AdicSystem.DerivedReductionProIso.reductionComplexSystem I M ⋙
        DerivedCategory.Q))

Stacks.LocalCohomology.UniformityII.isZero_tor_quotient_pow_idealOfVars, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityII/PolynomialQuotientTorDimension.lean, line 228. The attribute's comment: “in the standard example, A[x₁, …, x_r]/(x₁, …, x_r)ⁿ has tor dimension at most r for all n”.

A[x₁, …, x_r]/(x₁, …, x_r)ⁿ has Tor dimension at most r for all n: for every module N over R = A[x₁, …, x_r] and every p > r, Tor_p^R(R/(x₁, …, x_r)ⁿ, N) = 0.

theorem isZero_tor_quotient_pow_idealOfVars (n : ℕ) (N : ModuleCat.{u} (MvPolynomial (Fin r) A))
    {p : ℕ} (hp : r < p) :
    IsZero (((Tor' (ModuleCat.{u} (MvPolynomial (Fin r) A)) p).obj
      (ModuleCat.of _ (MvPolynomial (Fin r) A ⧸ idealOfVars (Fin r) A ^ n))).obj N)

Stacks.LocalCohomology.UniformityII.polynomialSystemFourIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityII/PolynomialSystemFour.lean, line 222. The attribute's comment: “the standard example: M ⊗ᴸ_P P/Jⁿ = M ⊗ᴸ_{A[x]} A[x]/(x)ⁿ for P = ℤ[x₁, …, x_r]”.

M ⊗ᴸ_P P/Jⁿ = M ⊗ᴸ_{A[x]} A[x]/(x)ⁿ. Let P = R₀[x₁, …, x_r] (the source takes R₀ = ℤ; at a universe u other than 0 one takes R₀ = ULift ℤ), let P → A send xᵢ to gᵢ, and J = (x₁, …, x_r). Then the system (4) n ↦ M ⊗ᴸ_P P/Jⁿ⁺¹ is isomorphic, as an inverse system in D(A), to the system n ↦ M ⊗ᴸ_{A[x]} A[x]/(x)ⁿ⁺¹, i.e. to the system (4) for A[x] → A, xᵢ ↦ gᵢ.

noncomputable def polynomialSystemFourIso :
    systemFour (polyEval R₀ g) M (MvPolynomial.idealOfVars (Fin r) R₀) ≅
      systemFour (polyEvalBase g) M (MvPolynomial.idealOfVars (Fin r) A)

Stacks.LocalCohomology.UniformityII.nonempty_proIso_polynomialSystemFour_systemTwo, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityII/PolynomialSystemFour.lean, line 236. The attribute's comment: “the standard example P = ℤ[x₁, …, x_r]: the system (4) is strictly pro-isomorphic to the system (2), by reduction to the finite map A[x] → A”.

In the situation of polynomialSystemFourIso, with A Noetherian and I = (g₁, …, g_r), the system (4) n ↦ M ⊗ᴸ_P P/Jⁿ⁺¹ for P = R₀[x₁, …, x_r] is strictly pro-isomorphic to the system (2) n ↦ M ⊗ᴸ_A A/Iⁿ⁺¹.

theorem nonempty_proIso_polynomialSystemFour_systemTwo [IsNoetherianRing A] :
    Nonempty (proObj (systemFour (polyEval R₀ g) M (MvPolynomial.idealOfVars (Fin r) R₀)) ≅
      proObj (systemTwo (polyEval R₀ g) M (Ideal.span (Set.range g))))

Stacks.LocalCohomology.UniformityII.isIso_proHom_derivedReductionComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityII/StrictDerivedReduction.lean, line 135. The attribute's comment: “the natural map from (2) to (1) is a strict pro-isomorphism”.

The natural map from system (2) to system (1) is a strict pro-isomorphism. Let I be an ideal of a Noetherian ring A, let M be a bounded complex of finite A-modules and p : P ⟶ M a quasi-isomorphism from a bounded above complex of finite flat modules, so that P/IⁿP computes M ⊗ᴸ_A A/Iⁿ. Then the natural map from the inverse system n ↦ P/I^(n+1)P to the inverse system n ↦ M/I^(n+1)M in D(A) is an isomorphism in the strict pro-category of D(A).

theorem isIso_proHom_derivedReductionComparison [IsNoetherianRing A] (I : Ideal A)
    (M : CochainComplex (ModuleCat.{u} A) ℤ)
    (hMbounded : ∃ a b : ℤ, M.IsStrictlyGE a ∧ M.IsStrictlyLE b)
    (hMfinite : ∀ i : ℤ, Module.Finite A (M.X i))
    {P : CochainComplex (ModuleCat.{u} A) ℤ} (p : P ⟶ M) (hPbounded : ∃ b : ℤ, P.IsStrictlyLE b)
    (hPfinite : ∀ i : ℤ, Module.Finite A (P.X i) ∧ Module.Flat A (P.X i))
    (hp : IsIso (DerivedCategory.Q.map p)) :
    IsIso (proHom (⟨0, Functor.whiskerRight (reductionComplexSystemMap I p) DerivedCategory.Q⟩ :
      StrictProHomRep (reductionComplexSystem I P ⋙ DerivedCategory.Q)
        (reductionComplexSystem I M ⋙ DerivedCategory.Q)))

Stacks.LocalCohomology.UniformityII.derivedReductionComparison_hasEventualInverses, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityII/StrictDerivedReduction.lean, line 154. The attribute's comment: “the systems (1) and (2) are pro-isomorphic, via Lemma 15.102.3”.

The systems (1) and (2) are pro-isomorphic. Let I be an ideal of a Noetherian ring A, let M be a bounded complex of finite A-modules and p : P ⟶ M a quasi-isomorphism from a bounded above complex of finite flat modules, so that P/IⁿP computes M ⊗ᴸ_A A/Iⁿ. Then the natural map from the system (2) n ↦ P/I^(n+1)P to the system (1) n ↦ M/I^(n+1)M in D(A) is a pro-isomorphism.

theorem derivedReductionComparison_hasEventualInverses [IsNoetherianRing A] (I : Ideal A)
    (M : CochainComplex (ModuleCat.{u} A) ℤ)
    (hMbounded : ∃ a b : ℤ, M.IsStrictlyGE a ∧ M.IsStrictlyLE b)
    (hMfinite : ∀ i : ℤ, Module.Finite A (M.X i))
    {P : CochainComplex (ModuleCat.{u} A) ℤ} (p : P ⟶ M) (hPbounded : ∃ b : ℤ, P.IsStrictlyLE b)
    (hPfinite : ∀ i : ℤ, Module.Finite A (P.X i) ∧ Module.Flat A (P.X i))
    (hp : IsIso (DerivedCategory.Q.map p)) :
    NoetherianAdicCompletion.HasEventualInverses
      (Functor.whiskerRight (reductionComplexSystemMap I p) DerivedCategory.Q)

Stacks.LocalCohomology.UniformityII.proIso_koszulToAdic, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityII/StrictnessFailure.lean, line 150. The attribute's comment: “the pro-isomorphism, in the category of modules, between the system H⁰(Kₙ) = A/(f₀ⁿ, …, f_{r-1}ⁿ) and the system A/Iⁿ, which is the comparison the remark makes by comparing with Koszul complexes and whose strictness the remark then denies”.

The two systems are isomorphic as pro-objects. The comparison koszulToAdic admits, at every level n, a two-sided inverse defined on a later level m: both triangles it forms with the transition maps commute.

public theorem proIso_koszulToAdic {A : Type u} [CommRing A] {r : ℕ} (f : Fin r → A) (n : ℕ) :
    ∃ (m : ℕ) (h : n ≤ m)
      (s : (AdicCompletionTor.idealPowerQuotientModuleSystem
              (Ideal.span (Set.range f))).obj (op m) ⟶
        (Koszul.powQuotientSystem f).obj (op n)),
      (koszulToAdic f).app (op m) ≫ s = (Koszul.powQuotientSystem f).map (homOfLE h).op ∧
        s ≫ (koszulToAdic f).app (op n)
          = (AdicCompletionTor.idealPowerQuotientModuleSystem
              (Ideal.span (Set.range f))).map (homOfLE h).op

Stacks.LocalCohomology.UniformityII.not_annihilator_pow_mul_pred, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityII/StrictnessFailure.lean, line 285. The attribute's comment: “the computation the remark performs on its example: for A = ℤ[x₀, …, x_{r-1}] and f i = x i, the module H⁰(Kₙ) = A/(x₀ⁿ, …, x_{r-1}ⁿ) is not annihilated by I^{r(n-1)}, witnessed by the monomial x₀^(n-1) ⋯ x_{r-1}^(n-1)”.

In ℤ[x₀, …, x_{r-1}] the module H⁰(Kₙ) = ℤ[x]/(x₀ⁿ, …, x_{r-1}ⁿ) is not annihilated by I^{r(n-1)}.

public theorem not_annihilator_pow_mul_pred (r n : ℕ) (hn : 1 ≤ n) :
    ¬ (monomialIdeal r ^ (r * (n - 1)) ≤
        Module.annihilator (MvPolynomial (Fin r) ℤ)
          (MvPolynomial (Fin r) ℤ ⧸
            Ideal.span (Set.range fun i : Fin r => (X i : MvPolynomial (Fin r) ℤ) ^ n)))

Stacks.LocalCohomology.UniformityII.not_strictProIso_monomial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityII/StrictnessFailure.lean, line 317. The attribute's comment: “the failure of strictness the remark asserts for systems (1) and (3) at M = A[0]: the system H⁰(Kₙ) = A/(x₀ⁿ, …, x_{r-1}ⁿ) over A = ℤ[x₀, …, x_{r-1}] admits no strict pro-isomorphism with the system A/Iⁿ, proved as the negation it is”.

Failure of strictness. For r ≥ 2 the inverse system H⁰(Kₙ) = ℤ[x]/(x₀ⁿ, …, x_{r-1}ⁿ) of the Koszul complexes on the powers of the variables and the adic system ℤ[x]/Iⁿ of the ideal I = (x₀, …, x_{r-1}) they generate are not strictly pro-isomorphic: there is no pair of strict pro-morphisms between them, in either direction, whose composite is eventually the identity of the Koszul system.

public theorem not_strictProIso_monomial (r : ℕ) (hr : 2 ≤ r) :
    ¬ ∃ (φ : StrictProHomRep
          (AdicCompletionTor.idealPowerQuotientModuleSystem
            (Ideal.span (Set.range fun i : Fin r => (X i : MvPolynomial (Fin r) ℤ))))
          (Koszul.powQuotientSystem fun i : Fin r => (X i : MvPolynomial (Fin r) ℤ)))
        (ψ : StrictProHomRep
          (Koszul.powQuotientSystem fun i : Fin r => (X i : MvPolynomial (Fin r) ℤ))
          (AdicCompletionTor.idealPowerQuotientModuleSystem
            (Ideal.span (Set.range fun i : Fin r => (X i : MvPolynomial (Fin r) ℤ))))),
      (ψ.comp φ).Equivalent
        (StrictProHomRep.id (Koszul.powQuotientSystem fun i : Fin r =>
          (X i : MvPolynomial (Fin r) ℤ)))

Stacks.LocalCohomology.UniformityII.not_nonempty_iso_proObj_monomial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityII/StrictnessFailure.lean, line 341. The attribute's comment: “the failure of strictness for systems (1) and (3) at M = A[0], stated as non-isomorphism of the two inverse sequences in the strict pro-category itself”.

Failure of strictness, in the strict pro-category. For r ≥ 2 the inverse sequence A/Iⁿ and the inverse sequence H⁰(Kₙ) = A/(x₀ⁿ, …, x_{r-1}ⁿ) over A = ℤ[x₀, …, x_{r-1}] are not isomorphic as objects of the strict pro-category.

public theorem not_nonempty_iso_proObj_monomial (r : ℕ) (hr : 2 ≤ r) :
    ¬ Nonempty
      (proObj (AdicCompletionTor.idealPowerQuotientModuleSystem
          (Ideal.span (Set.range fun i : Fin r => (X i : MvPolynomial (Fin r) ℤ)))) ≅
        proObj (Koszul.powQuotientSystem fun i : Fin r =>
          (X i : MvPolynomial (Fin r) ℤ)))

Stacks.LocalCohomology.UniformityII.not_nonempty_iso_proObj_derived_monomial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityII/StrictnessFailureDerived.lean, line 120. The attribute's comment: “systems (1) and (3) are not strictly pro-isomorphic, even for M = A[0]: the example A = ℤ[x₁, …, x_r], fᵢ = xᵢ, read in the strict pro-category of D(A)”.

Stacks 0GA5, failure of strictness for (1) and (3), in D(A). Let A = ℤ[x₀, …, x_{r-1}] with r ≥ 2, fᵢ = xᵢ and I = (x₀, …, x_{r-1}). For M = A[0] the system (1) is n ↦ (A/I^(n+1))[0] and the system (3) is n ↦ A ⊗ᴸ K_{n+1} = K_{n+1}, the Koszul complex on x₀^(n+1), …, x_{r-1}^(n+1). These two inverse systems of D(A) are not isomorphic in the strict pro-category of D(A).

Applying H⁰ to an isomorphism of the strict pro-category gives one between the systems A/I^(n+1) and H⁰(K_{n+1}) = A/(x₀^(n+1), …, x_{r-1}^(n+1)) of modules, which not_nonempty_iso_proObj_monomial rules out.

theorem not_nonempty_iso_proObj_derived_monomial {r : ℕ}
    [HasDerivedCategory.{w} (ModuleCat.{0} (MvPolynomial (Fin r) ℤ))] (hr : 2 ≤ r) :
    ¬ Nonempty
      (proObj (AdicCompletionTor.idealPowerQuotientModuleSystem
          (Ideal.span (Set.range fun i : Fin r => (X i : MvPolynomial (Fin r) ℤ))) ⋙
          DerivedCategory.singleFunctor (ModuleCat.{0} (MvPolynomial (Fin r) ℤ)) 0) ≅
        proObj (Koszul.powDerivedSystem fun i : Fin r => (X i : MvPolynomial (Fin r) ℤ)))

CategoryTheory.StrictProCategory, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityII/StrictProCategory.lean, line 32. The attribute's comment: “strict_pro_category”.

The strict pro-category of C. Its objects are inverse sequences in C; its morphisms are uniformly shifted compatible maps modulo eventual agreement after passing to a common shift.

abbrev StrictProCategory (C : Type u) [Category.{v} C]

Stacks.LocalCohomology.UniformityII.derivedTensorKoszulSystem_hasEventualInverses, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityII/StrictProFourSystems.lean, line 70. The attribute's comment: “the pro-isomorphism between the systems (2) and (3), via Lemma 15.96.1”.

Systems (2) and (3) are pro-isomorphic. For an ideal I = (f₀, …, f_{r-1}) of a Noetherian ring A, the inverse system n ↦ M ⊗ᴸ K_{n+1} of derived tensor products with the Koszul complexes on the positive powers of the generators is pro-isomorphic to the inverse system n ↦ M ⊗ᴸ A/Iⁿ⁺¹, via the derived tensor product with M of the comparison Kₙ → A/Iⁿ of [Stacks, Tag 0921].

public theorem derivedTensorKoszulSystem_hasEventualInverses
    [IsNoetherianRing A] {r : ℕ} (f : Fin r → A) (I : Ideal A)
    (hI : I = Ideal.span (Set.range f))
    (T : CochainComplex.DerivedTensor.DerivedTensorProduct A)
    (M : CochainComplex (ModuleCat.{u} A) ℤ) :
    NoetherianAdicCompletion.HasEventualInverses
      (Functor.whiskerRight (NoetherianAdicCompletion.koszulIdealPowerComparison f I hI)
        (T.tensor.obj (DerivedCategory.Q.obj M)))

Stacks.LocalCohomology.UniformityII.derivedTensorKoszulSystem_hasEventualInverses_canonical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityII/StrictProFourSystems.lean, line 84. The attribute's comment: “the pro-isomorphism between the systems (2) and (3), for the canonical derived tensor product”.

derivedTensorKoszulSystem_hasEventualInverses for the canonical derived tensor product of [Stacks, Tag 0BYI].

public theorem derivedTensorKoszulSystem_hasEventualInverses_canonical
    [IsNoetherianRing A] {r : ℕ} (f : Fin r → A) (I : Ideal A)
    (hI : I = Ideal.span (Set.range f))
    (M : CochainComplex (ModuleCat.{u} A) ℤ) :
    NoetherianAdicCompletion.HasEventualInverses
      (Functor.whiskerRight (NoetherianAdicCompletion.koszulIdealPowerComparison f I hI)
        ((CochainComplex.DerivedTensor.canonicalDerivedTensorProduct A).tensor.obj
          (DerivedCategory.Q.obj M)))

Stacks.LocalCohomology.UniformityII.isIso_proHom_systemFourToTwo, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityII/StrictSystemFour.lean, line 156. The attribute's comment: “if P → A is finite, the system (4) is strictly pro-isomorphic to the system (2)”.

Stacks 0GA5: if P → A is finite, system (4) is strictly pro-isomorphic to system (2). Let P be Noetherian, f : P → A a finite ring map, J ⊆ P an ideal with I = JA, and M a complex of A-modules. Then the comparison from the system n ↦ M ⊗ᴸ_P P/Jⁿ⁺¹ to the system n ↦ M ⊗ᴸ_A A/Iⁿ⁺¹ is an isomorphism of the strict pro-category of D(A).

The source states the remark for a bounded complex M of finite modules over a Noetherian ring A; neither hypothesis is used here.

theorem isIso_proHom_systemFourToTwo [IsNoetherianRing P] (hf : f.Finite) (J : Ideal P)
    (I : Ideal A) (hI : I = J.map f) :
    IsIso (proHom (⟨0, systemFourToTwo f M J I hI⟩ :
      StrictProHomRep (systemFour f M J) (systemTwo f M I)))

Stacks.LocalCohomology.UniformityII.hasUniformInverses_systemTwoToOne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityII/StrictSystemTwo.lean, line 257. The attribute's comment: “the natural map from (2) to (1) is a strict pro-isomorphism, for (2) formed with the derived tensor product”.

The natural map from (2) to (1) is a strict pro-isomorphism, for the derived-tensor model of (2). Let I be an ideal of a Noetherian ring A and M a bounded complex of finite A-modules. The counits M ⊗ᴸ_A A/Iⁿ⁺¹ ⟶ M/Iⁿ⁺¹M have inverses over a shift independent of n.

theorem hasUniformInverses_systemTwoToOne [IsNoetherianRing A] (I : Ideal A)
    (hMbounded : ∃ a b : ℤ, M.IsStrictlyGE a ∧ M.IsStrictlyLE b)
    (hMfinite : ∀ i : ℤ, Module.Finite A (M.X i)) :
    HasUniformInverses (systemTwoToOne f M I)

Stacks.AdicSystem.DerivedReductionProIso.derivedReduction_exists_uniform_inverse, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/RingTheory/Module/AdicSystem/UniformDerivedReduction.lean, line 499. The attribute's comment: “the natural map from (2) to (1) is a strict pro-isomorphism: inverses over a uniform shift”.

[Stacks, Tag 0GA5], explicitly. In the situation of derivedReduction_hasUniformInverses, there is a shift c such that for all n + c ≤ m the comparison maps adicReductionComparison acquire an inverse from level m to level n whose two round trips are the transition maps.

theorem derivedReduction_exists_uniform_inverse [IsNoetherianRing A] (I : Ideal A)
    (M : CochainComplex (ModuleCat.{u} A) ℤ)
    (hMbounded : ∃ a b : ℤ, M.IsStrictlyGE a ∧ M.IsStrictlyLE b)
    (hMfinite : ∀ i : ℤ, Module.Finite A (M.X i))
    {P : CochainComplex (ModuleCat.{u} A) ℤ} (p : P ⟶ M) (hPbounded : ∃ b : ℤ, P.IsStrictlyLE b)
    (hPfinite : ∀ i : ℤ, Module.Finite A (P.X i) ∧ Module.Flat A (P.X i))
    (hp : IsIso (DerivedCategory.Q.map p)) :
    ∃ c : ℕ, ∀ n m : ℕ, n + c ≤ m →
      ∃ (h : n ≤ m) (s : DerivedCategory.Q.obj ((reduceComplex (I ^ (m + 1))).obj M) ⟶
          DerivedCategory.Q.obj ((reduceComplex (I ^ (n + 1))).obj P)),
        adicReductionComparison I p m ≫ s = adicReductionTransition I P h ∧
          s ≫ adicReductionComparison I p n = adicReductionTransition I M h

Sources

• Section 51.21, Tag 0G9W
• AxiomMath/Stacks at 5ed82d14

Leanexists_uniform_tor_transition_eq_zero_of_pow_smul_eq_bot · Stacks.Blowup.exists_pow_le_annihilator_tor_affineBlowupAlgebra · Stacks.Blowup.exists_threshold_nonempty_derivedGlobalSectionsTwistedPullback_iso_derivedTensorIdealPow · Stacks.Blowup.exists_pow_le_annihilator_homology_derivedPullback · Stacks.LocalCohomology.UniformityII.exists_pow_le_annihilator_tor_quotient_pow_blowup · Stacks.LocalCohomology.UniformityII.exists_pow_le_annihilator_tor_quotient_pow · Stacks.LocalCohomology.UniformityII.exists_pow_le_annihilator_tor_quotient_pow_of_card_le_one · exists_uniform_tor_transition_eq_zero_of_pow_le_annihilator_tor'

Section51.22 A bit of uniformity, III#

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

Tag 0GA6, the section

Tag 0GA6 in the Stacks Project.

AssociatedGraded.dInvariant, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/AssociatedGradedInvariants.lean, line 126. The attribute's comment: “the invariant d(S) of the associated graded ring S = Gr_I(A), as the maximum of the dimensions of the fibres of Proj(S) → Spec(S₀), which is clause (2) of the paragraph defining d; the equality with the maximum of the fibre dimensions of the blowup p : X → Spec(A), the paragraph's primary phrasing, is not proved here”.

The invariant d(S) = d(Gr_I(A)): the maximum of the dimensions of the fibres of Proj(S) → Spec(S₀), a fibre with empty underlying space contributing 0.

This is clause (2) of the paragraph of [Stacks, Tag 0GA6] that introduces d; see the implementation notes for its relation to the paragraph's primary phrasing in terms of the blowup.

def dInvariant : ℕ∞

AssociatedGraded.qInvariant, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/AssociatedGradedInvariants.lean, line 166. The attribute's comment: “the invariant q(S) of the associated graded ring S = Gr_I(A), as the smallest q(S) ≥ 0 such that for all q ≥ q(S) one has Hⁱ(Y, 𝒪_Y(q)) = 0 for 1 ≤ i ≤ d(S) and H⁰(Y, 𝒪_Y(q)) = I^q/I^{q+1} for Y = Proj(S); the appeal to Cohomology of Schemes Lemmas 0AG6 and 0AG7 that makes the set of such bounds nonempty is not proved here, and is carried as a hypothesis by isRegularDegree_of_qInvariant_le”.

The invariant q(S) = q(Gr_I(A)): the smallest q₀ ≥ 0 such that AssociatedGraded.IsRegularDegree holds at every q ≥ q₀.

That the set of such q₀ is nonempty is Cohomology of Schemes, Lemmas [Stacks, Tag 0AG6] and [Stacks, Tag 0AG7], which are not available in this generality; it is therefore a hypothesis of AssociatedGraded.isRegularDegree_of_qInvariant_le and not proved here.

def qInvariant : ℕ

Tag 0GA7, a lemma

Tag 0GA7 in the Stacks Project.

Stacks.LocalCohomology.UniformityIII.blowupHmod_of_qS_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityIII/BlowupSituation.lean, line 705.

[Stacks, Tag 0GA7]: with q₀ = q(S) (qS I, the least integer such that for all q ≥ q₀ one has Hⁱ(Y, 𝒪_Y(q)) = 0 for i ≥ 1 and H⁰(Y, 𝒪_Y(q)) = Iᑫ/I^{q+1}), for a Noetherian ring A and any ideal I, on the blowup X of Spec A in I:

1. for n ≥ 1, q ≥ q₀ and i > 0, Hⁱ(X, 𝒪_{Yₙ}(q)) = 0;
2. for n ≥ 1 and q ≥ q₀, the canonical map Iᑫ/I^{q+n} → H⁰(X, 𝒪_{Yₙ}(q)) is an isomorphism — stated as the bijectivity of cdivMod I m q, whose source is Iᑫ/I^{q+m+1} and whose target is H⁰(X, 𝒪_{Y_{m+1}}(q)), for every m, i.e. at n = m + 1;
3. for q ≥ q₀ and i > 0, Hⁱ(X, 𝒪_X(q)) = 0;
4. for q ≥ q₀, the canonical map Iᑫ → H⁰(X, 𝒪_X(q)) is an isomorphism.

The cohomology is A-module-valued, the source's identifications being isomorphisms of A-modules. The integer d = d(S) the tag names enters only through the definition of q(S), where it bounds the degrees in which vanishing is asked; see IsBaseThreshold, isBaseThreshold_iff_of_vanishing_gt and exists_qS_isLeast_isBaseThresholdUpTo.

theorem blowupHmod_of_qS_le [IsNoetherianRing A] :
    (∀ n i q : ℕ, 1 ≤ n → 1 ≤ i → qS I ≤ q →
        Subsingleton (blowupHmod I i (thickeningTwist I n q))) ∧
      (∀ n q : ℕ, qS I ≤ q → Function.Bijective (cdivMod I n q)) ∧
      (∀ i q : ℕ, 1 ≤ i → qS I ≤ q → Subsingleton (blowupHmod I i (blowupTwist I q))) ∧
      (∀ q : ℕ, qS I ≤ q → Function.Bijective (ambientSectionsMod I q))

Tag 0GA8, a lemma

Tag 0GA8 in the Stacks Project.

AlgebraicGeometry.exceptionalIdeal_pow_le_annihilator_kernel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/AlmostExactness.lean, line 421.

In a short exact sequence over A ⧸ I ^ n whose quotient is finite and I ^ c / I ^ n-projective, the kernel of the pulled-back first map is annihilated by the ideal of the c-th exceptional thickening.

public theorem exceptionalIdeal_pow_le_annihilator_kernel
    {A : Type u} [CommRing A] (I : Ideal A) (n c : ℕ) (_hcn : c ≤ n)
    (K L M : ModuleCat.{u} (A ⧸ I ^ n))
    (f : K ⟶ L) (g : L ⟶ M) (w : f ≫ g = 0)
    (hExact : (ShortComplex.mk f g w).ShortExact)
    [Module.Finite (A ⧸ I ^ n) M]
    (hM : Module.IsIProjective (A ⧸ I ^ n)
      (Ideal.map (Ideal.Quotient.mk (I ^ n)) (I ^ c)) M) :
    (exceptionalIdeal (Scheme.IdealSheafData.ofIdealTop
      (Ideal.map (Scheme.ΓSpecIso (.of A)).inv.hom I))) ^ c ≤
      Scheme.Modules.annihilatorIdeal
        (kernel ((Scheme.Modules.pullback
          (blowUpToBase (Scheme.IdealSheafData.ofIdealTop
            (Ideal.map (Scheme.ΓSpecIso (.of A)).inv.hom I)))).map
              ((tilde.functor (.of A)).map
              ((ModuleCat.restrictScalars (Ideal.Quotient.mk (I ^ n))).map f))))

Tag 0GA9, a lemma

Tag 0GA9 in the Stacks Project.

AlgebraicGeometry.schemeTheoreticSupport_iff_exceptionalTwistContraction_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Blowup/ExceptionalTwist.lean, line 227. The attribute's comment: “corrected: the canonical map runs 𝓕(c) ⟶ 𝓕, since 𝒪(1) is the ideal sheaf of Y”.

Stacks Project, Tag 0GA9. A quasi-coherent module of finite type on the blowup of a scheme in a quasi-coherent sheaf of ideals is scheme theoretically supported on the c-fold thickening Y_c of the exceptional divisor if and only if the canonical map 𝓕(c) ⟶ 𝓕 vanishes.

theorem schemeTheoreticSupport_iff_exceptionalTwistContraction_eq_zero
    (F : (blowUp ℐ).Modules) [F.IsQuasicoherent] [F.IsFiniteType] :
    exceptionalIdeal ℐ ^ c ≤ Scheme.Modules.schemeTheoreticSupport F ↔
      exceptionalTwistContraction ℐ c F = 0

Tag 0GAA, a lemma

Tag 0GAA in the Stacks Project.

Stacks.LocalCohomology.UniformityIII.ModuleSituation.subsingleton_H_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityIII/PullbackCohomology.lean, line 591. The attribute's comment: “clause (1), H^d(X, p^*M(q)) = 0 for i = d ≥ 1 and q ≥ q₀”.

Stacks Project, Tag 0GAA, clause (1). For an (A, n, c)-module M, in the case i = d ≥ 1 and q ≥ q₀ we have H^d(X, p^*M(q)) = 0.

The long exact sequence of 0 → 𝒢 → (𝒪_{Yₙ})^{⊕r} → p^*M → 0 sits H^d(X, p^*M(q)) between H^d(X, (𝒪_{Yₙ})^{⊕r}(q)), which vanishes by Tag 0GA7(1), and H^{d+1}(X, 𝒢(q)), which vanishes because d bounds the fibre dimensions.

theorem subsingleton_H_top (M : ANCModule I n c) {q : ℤ}
    (hd : 1 ≤ S.d) (hq : (S.q₀ : ℤ) ≤ q) : Subsingleton (S.H M S.d q)

Stacks.LocalCohomology.UniformityIII.ModuleSituation.subsingleton_H_next, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityIII/PullbackCohomology.lean, line 616. The attribute's comment: “clause (2), H^{d-1}(X, p^*M(q)) = 0 for i = d - 1 ≥ 1 and q ≥ q₀”.

Stacks Project, Tag 0GAA, clause (2). For an (A, n, c)-module M, in the case i = d - 1 ≥ 1 and q ≥ q₀ we have H^{d-1}(X, p^*M(q)) = 0.

The long exact sequence of 0 → 𝒢 → (𝒪_{Yₙ})^{⊕r} → p^*M → 0 sits H^{d-1}(X, p^*M(q)) between H^{d-1}(X, (𝒪_{Yₙ})^{⊕r}(q)), which vanishes by Tag 0GA7(1) since d - 1 ≥ 1, and H^d(X, 𝒢(q)), which vanishes by subsingleton_HG_top.

The hypothesis i = d - 1 is written i + 1 = d to avoid a truncated subtraction.

theorem subsingleton_H_next (M : ANCModule I n c) {i : ℕ} {q : ℤ}
    (hi : 1 ≤ i) (hid : i + 1 = S.d) (hq : (S.q₀ : ℤ) ≤ q) : Subsingleton (S.H M i q)

Stacks.LocalCohomology.UniformityIII.TwistedModuleSituation.Htr_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityIII/PullbackCohomology.lean, line 863. The attribute's comment: “clause (3), Hⁱ(X, p^M(q)) → Hⁱ(X, p^M(q-(d-1-i)c)) is zero for d-1 > i > 0”.

Stacks Project, Tag 0GAA, clause (3). For an (A, n, c)-module M, in the case d - 1 > i > 0 and q ≥ q₀ + (d - 1 - i)c the map Hⁱ(X, p^*M(q)) → Hⁱ(X, p^*M(q - (d - 1 - i)c)) is zero.

The case distinction d - 1 > i > 0 is written 1 ≤ i together with i + k + 1 = d and 1 ≤ k, which fixes k = d - 1 - i; the target twist q - kc is carried as a parameter r with r + kc = q. The proof reduces the statement to HGtr_eq_zero, whose induction it is.

theorem Htr_eq_zero (M : ANCModule I n c) {i k : ℕ} {q r : ℤ} (h : r ≤ q)
    (hi : 1 ≤ i) (hk : 1 ≤ k) (hik : i + k + 1 = S.d) (hr : r + k * c = q)
    (hq : (S.q₀ : ℤ) + k * c ≤ q) : S.Htr M i q r h = 0

Stacks.LocalCohomology.UniformityIII.TwistedModuleSituation.surjective_secM, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityIII/PullbackCohomology.lean, line 899. The attribute's comment: “clause (4), surjectivity onto H⁰(X, p^*M(q)) for i = 0, d ≤ 1, q ≥ q₀; corrected: the source is I^q ⊗_A M, not the submodule I^qM, for which this is false”.

Stacks Project, Tag 0GAA, clause (4). For an (A, n, c)-module M, in the case i = 0, d ∈ {0, 1} and q ≥ q₀ the canonical map I^q ⊗_A M → H⁰(X, p^*M(q)) is surjective.

The long exact sequence of 0 → ℱ → p^*K → 𝒢 → 0 makes H¹(X, p^*K(q)) → H¹(X, 𝒢(q)) surjective, since H²(X, ℱ(q)) = 0 for d ≤ 1; its source vanishes, by clause (1) if d = 1 and because d bounds the fibre dimensions if d = 0. So H¹(X, 𝒢(q)) = 0 and the long exact sequence of 0 → 𝒢 → (𝒪_{Yₙ})^{⊕r} → p^*M → 0 makes H⁰(X, (𝒪_{Yₙ})^{⊕r}(q)) → H⁰(X, p^*M(q)) surjective; for q ≥ q₀ the source is (I^q/I^{q+n})^{⊕r} by Tag 0GA7(2), and the composite with it factors through I^q ⊗_A M by ANCPresentation.freeTensor_surjective.

The Stacks Project writes the source I^qM. Read as the submodule I^q·M of M the clause is false: for A = ℤ, I = (2) (so the blowing up is an isomorphism, d = 0, q₀ = 0), n = 1, c = 0 and M = A ⧸ I, at q = 1 that submodule is 0 while Tag 0GA7(2) gives H⁰(X, p^*M(1)) = H⁰(X, 𝒪_{Y₁}(1)) = I/I² ≅ ℤ/2. What the proof produces, and what is formalized, is the surjection out of I^q ⊗_A M = (I^q/I^{q+n}) ⊗_A M, which agrees with I^q/I^{q+n} for M = A ⧸ Iⁿ as Tag 0GA7(2) demands.

theorem surjective_secM (M : ANCModule I n c) {q : ℕ} (hd : S.d ≤ 1) (hq : S.q₀ ≤ q) :
    Function.Surjective (S.secM M q)

Stacks.LocalCohomology.UniformityIII.TwistedModuleSituation.range_Htr_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityIII/PullbackCohomology.lean, line 930. The attribute's comment: “clause (5), H⁰(p^M(q)) → H⁰(p^M(q-(d-1)c)) lands in the image of the canonical map out of I^{q-(d-1)c} ⊗_A M; corrected as in clause (4)”.

Stacks Project, Tag 0GAA, clause (5). For an (A, n, c)-module M, in the case i = 0, d > 1 and q ≥ q₀ + (d - 1)c the image of H⁰(X, p^*M(q)) → H⁰(X, p^*M(q - (d - 1)c)) is contained in the image of the canonical map I^{q - (d-1)c} ⊗_A M → H⁰(X, p^*M(q - (d - 1)c)), the map of clause (4); as there, the source is the tensor product and not the submodule I^{q-(d-1)c}M of M.

The case d > 1 is written k + 1 = d with 1 ≤ k, which fixes k = d - 1; the target twist q - kc is carried as a natural number r with r + kc = q, which is no restriction since q ≥ q₀ + kc forces q - kc ≥ q₀ ≥ 0. Arguing as in clause (4) it suffices that the image lie in the image of H⁰(X, (𝒪_{Yₙ})^{⊕r}(q - (d-1)c)), which by the long exact sequence of 0 → 𝒢 → (𝒪_{Yₙ})^{⊕r} → p^*M → 0 holds as soon as the boundary in H¹(X, 𝒢(q)) dies in H¹(X, 𝒢(q - (d-1)c)); that is HGtr_eq_zero at i = 0.

theorem range_Htr_le (M : ANCModule I n c) {k r : ℕ} {q : ℤ} (h : (r : ℤ) ≤ q)
    (hk : 1 ≤ k) (hkd : k + 1 = S.d) (hr : (r : ℤ) + k * c = q)
    (hq : (S.q₀ : ℤ) + k * c ≤ q) :
    LinearMap.range (S.Htr M 0 q (r : ℤ) h) ≤ LinearMap.range (S.secM M r)

Tag 0GAB, a remark

Tag 0GAB in the Stacks Project.

Stacks.SheafOfModules.PullbackDual.dualModuleSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Duality/PullbackOfDualSheaf.lean, line 119. The attribute's comment: “the dual F^∨ = SheafHom(F, O), for a sheaf of modules on a ringed site”. References: EGA 0 (4.1.5); SGA 3 I (4.6.5.1), “more general”; SGA 3 III (0.6); SGA 3 VIIA (4.3.3), “more general”.

The dual F^∨ = SheafHom_O(F, O) of a sheaf of modules on a ringed site: the internal Hom of Tag 03EM out of F into the structure sheaf, the structure sheaf being read as a module over itself. This is the (-)^∨ of Tag 0GAB.

noncomputable def dualModuleSheaf (Z : RingedSite.{u, u, u})
    (F : _root_.SheafOfModules.{u} (Tensor.ringSheaf Z.O)) :
    _root_.SheafOfModules.{u} (Tensor.ringSheaf Z.O)

Stacks.LocalCohomology.UniformityIII.moduleDual, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityIII/DualPullback.lean, line 130. The attribute's comment: “the dual M^∨ = Hom_{A/Iⁿ}(M, A/Iⁿ) of a module over A/Iⁿ, and its functoriality”. References: SGA 3 VIIA (3.1.1), “affine dual object”; SGA 3 VIIA (4.3.3), “special case”; SGA 3 VIIB (1.3.5.C), “more general”; SGA 3 VIII (6.8).

The dual M^∨ = Hom_R(M, R) of an R-module, as a functor contravariant in M: on morphisms it is LinearMap.dualMap, that is, precomposition. For R = A/Iⁿ this is the M^∨ of Tag 0GAB; no finiteness of M is needed to form it.

noncomputable def moduleDual : (ModuleCat.{u} R)ᵒᵖ ⥤ ModuleCat.{u} R

Stacks.LocalCohomology.UniformityIII.IsANCModule.exists_finFree_factorization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityIII/DualPullback.lean, line 259. The attribute's comment: “for a ∈ I^c the map a : M → M factors through a finite free A/Iⁿ-module”.

Stacks Project, Tag 0GAB. For an (A, n, c)-module M and a ∈ I^c the multiplication-by-a endomorphism of M factors through a finite free A/Iⁿ-module.

This is the step the remark's proof of clause (4) opens with. By IsANCModule the map factors through a projective module; since M is finite it factors through a finite projective module by Tag 0G91, and a finite projective module is a retract of a finite free one.

theorem IsANCModule.exists_finFree_factorization {A : Type u} [CommRing A] {I : Ideal A}
    {n c : ℕ} {M : ModuleCat.{u} (A ⧸ I ^ n)} (hM : IsANCModule I n c M)
    {a : A ⧸ I ^ n} (ha : a ∈ Ideal.map (Ideal.Quotient.mk (I ^ n)) (I ^ c)) :
    ∃ (r : ℕ) (α : M ⟶ finFreeModule (A ⧸ I ^ n) r)
      (β : finFreeModule (A ⧸ I ^ n) r ⟶ M), α ≫ β = a • 𝟙 M

Stacks.LocalCohomology.UniformityIII.pullbackModuleDualMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityIII/DualPullbackSource.lean, line 314. The attribute's comment: “the canonical map can : p^(M^∨) ⟶ (p^M)^∨”.

Tag 0GAB, the canonical map can : p^*(M^∨) ⟶ (p^*M)^∨. For a morphism of ringed sites f : X ⟶ Spec R and an R-module M, with p^*N = f^*(N~): the pullback of the comparison (M^∨)~ ⟶ (M~)^∨, followed by the canonical map f^*((M~)^∨) ⟶ (f^*(M~))^∨ of Stacks.SheafOfModules.PullbackDual.pullbackDualMap.

noncomputable def pullbackModuleDualMap (M : ModuleCat.{u} R) :
    (ringedSitePullback f).obj ((specTilde R).obj ((moduleDual R).obj (op M))) ⟶
      dualModuleSheaf X ((ringedSitePullback f).obj ((specTilde R).obj M))

Stacks.LocalCohomology.UniformityIII.pullbackModuleDualMap_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityIII/DualPullbackSource.lean, line 322. The attribute's comment: “the construction of can is functorial in M”.

Tag 0GAB, the construction of can is functorial in M. For g : M ⟶ N the square formed by can at M and at N, by p^*(g^∨) and by (p^*g)^∨ commutes.

theorem pullbackModuleDualMap_naturality {M N : ModuleCat.{u} R} (g : M ⟶ N) :
    (ringedSitePullback f).map ((specTilde R).map ((moduleDual R).map g.op)) ≫
        pullbackModuleDualMap f M =
      pullbackModuleDualMap f N ≫
        dualModuleSheafMap X ((ringedSitePullback f).map ((specTilde R).map g))

Stacks.LocalCohomology.UniformityIII.isIso_pullbackModuleDualMap_finFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityIII/DualPullbackSource.lean, line 347. The attribute's comment: “can is an isomorphism at a finite free A/Iⁿ-module”.

Tag 0GAB: can is an isomorphism at a finite free module R^{⊕r}. The comparison is invertible there, R^{⊕r} being of finite presentation, and so is the sheaf-level can at (R^{⊕r})~, M ↦ M~ being additive with R~ = 𝒪.

theorem isIso_pullbackModuleDualMap_finFree (r : ℕ) :
    IsIso (pullbackModuleDualMap f (finFreeModule R r))

Stacks.LocalCohomology.UniformityIII.IsANCModule.kernel_map_pullbackModuleDualMap_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityIII/DualPullbackSource.lean, line 528. The attribute's comment: “for an (A,n,c)-module M, every a ∈ I^c annihilates the kernel of can”.

Tag 0GAB, the kernel of can. Let M be an (A, n, c)-module, a ∈ I^c and f : X ⟶ Spec(A/Iⁿ) any morphism of ringed sites. Then a annihilates the kernel of can : p^*(M^∨) ⟶ (p^*M)^∨: the endomorphism of ker(can) induced by multiplication by a on p^*(M^∨) and on (p^*M)^∨ is zero. The source's reason is the proof: a : M → M factors through a finite free A/Iⁿ-module (IsANCModule.exists_finFree_factorization), at which can is an isomorphism.

theorem IsANCModule.kernel_map_pullbackModuleDualMap_eq_zero {X : RingedSite.{u, u, u}}
    (f : RingedSite.Hom X (specRingedSite (CommRingCat.of (A ⧸ I ^ n))))
    {M : ModuleCat.{u} (A ⧸ I ^ n)} (hM : IsANCModule I n c M) {a : A ⧸ I ^ n}
    (ha : a ∈ Ideal.map (Ideal.Quotient.mk (I ^ n)) (I ^ c)) :
    letI := specLinear (CommRingCat.of (A ⧸ I ^ n))
    kernel.map (pullbackModuleDualMap f M) (pullbackModuleDualMap f M)
        ((ringedSitePullback f).map (a • 𝟙 ((specTilde (CommRingCat.of (A ⧸ I ^ n))).obj
          ((moduleDual (CommRingCat.of (A ⧸ I ^ n))).obj (op M)))))
        (dualModuleSheafMap X ((ringedSitePullback f).map
          (a • 𝟙 ((specTilde (CommRingCat.of (A ⧸ I ^ n))).obj M))))
        (pullbackModuleDualMap_smul_naturality f M a) = 0

Stacks.LocalCohomology.UniformityIII.IsANCModule.cokernel_map_pullbackModuleDualMap_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityIII/DualPullbackSource.lean, line 545. The attribute's comment: “for an (A,n,c)-module M, every a ∈ I^c annihilates the cokernel of can”.

Tag 0GAB, the cokernel of can. For an (A, n, c)-module M, a ∈ I^c and any morphism of ringed sites f : X ⟶ Spec(A/Iⁿ), a annihilates the cokernel of can : p^*(M^∨) ⟶ (p^*M)^∨.

theorem IsANCModule.cokernel_map_pullbackModuleDualMap_eq_zero {X : RingedSite.{u, u, u}}
    (f : RingedSite.Hom X (specRingedSite (CommRingCat.of (A ⧸ I ^ n))))
    {M : ModuleCat.{u} (A ⧸ I ^ n)} (hM : IsANCModule I n c M) {a : A ⧸ I ^ n}
    (ha : a ∈ Ideal.map (Ideal.Quotient.mk (I ^ n)) (I ^ c)) :
    letI := specLinear (CommRingCat.of (A ⧸ I ^ n))
    cokernel.map (pullbackModuleDualMap f M) (pullbackModuleDualMap f M)
        ((ringedSitePullback f).map (a • 𝟙 ((specTilde (CommRingCat.of (A ⧸ I ^ n))).obj
          ((moduleDual (CommRingCat.of (A ⧸ I ^ n))).obj (op M)))))
        (dualModuleSheafMap X ((ringedSitePullback f).map
          (a • 𝟙 ((specTilde (CommRingCat.of (A ⧸ I ^ n))).obj M))))
        (pullbackModuleDualMap_smul_naturality f M a) = 0

Tag 0GAC, a lemma

Tag 0GAC in the Stacks Project.

Stacks.LocalCohomology.UniformityIII.DualSituation.exists_sum_powQuotSmul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityIII/DivisibleMaps.lean, line 358. The attribute's comment: “with max(d, 1) in place of d, since at d = 0 the source's own argument reaches only level n - 2c while the source states n - c; its one open input is the level-(n-2c) section σ' of p^*(M^∨) produced by factoring through can, hypothesis hσ”.

Stacks Project, Tag 0GAC. With q₀ = q(S) and d = d(S), let M be an (A, n, c)-module and φ : M → Iⁿ/I^{2n} an A-linear map. Write D = max(d, 1) and assume n ≥ q₀ + (1 + D)c and n ≥ (2 + D)c. Then the composition

M --φ--> Iⁿ/I^{2n} → I^{n-(1+D)c}/I^{2n-(1+D)c}

is of the form ∑ aᵢψᵢ with aᵢ ∈ I^c and ψᵢ : M → I^{n-(2+D)c}/I^{2n-(2+D)c}.

The levels are carried as parameters so that no truncated subtraction appears in a type: k + 1 = D, g + c = f, f + kc = e and e + 2c = n, so that f = n - (1 + D)c, g = n - (2 + D)c and e = n - 2c; the two numerical hypotheses of the source are the existence of g as a natural number (n ≥ (2 + D)c) and q₀ ≤ f (n ≥ q₀ + (1 + D)c).

Deviation from the source, at d = 0. The source writes d where this statement writes D = max(d, 1), and adds for d = 0 the hypothesis n ≥ q₀ + 2c. For d ≥ 1 the two agree exactly. For d = 0 the source's own argument does not reach the level it asserts: it produces σ' at level n - 2c — the cost of factoring through can : p^*(M^∨) → (p^*M)^∨, whose kernel and cokernel are supported on Y_c, and which is independent of d — and then applies clause (4) of Tag 0GAA at that level, which gives no further drop, so the argument ends at n - 2c while the statement asserts n - (1 + 0)c = n - c, a discrepancy of c in the wrong direction. The source's extra hypothesis n ≥ q₀ + 2c for d = 0 is precisely what makes clause (4) applicable at n - 2c, which corroborates that n - 2c is the level reached. So for d = 0 the levels stated here are the ones the argument supports, namely the d = 1 numbers 2c and 3c; the hypothesis n ≥ 3c this needs is not implied by the source's d = 0 hypotheses and is therefore part of n ≥ (2 + D)c above. Twisting the identity proved here down by c recovers the source's numbering, so the source's d = 0 form is strictly stronger than what its argument establishes.

The one open input. The level-(n - 2c) section σ' is a hypothesis, not a conclusion: producing it is the duality step of the source, which rests on the kernel and cokernel of can being scheme-theoretically supported on Y_c — a statement about the blowup situation that Stacks.SheafOfModules.PullbackDual (Tag 0GAB) explicitly does not prove. Everything after it is derived: the (d-1)c drop is Tag 0GAA clause (5) for d ≥ 2 and clause (4) for d ≤ 1 (exists_ev_secM_eq), and the passage from the resulting element of I^f ⊗_A M^∨ to the sum ∑ aᵢψᵢ is ev_secM_mem_divisibleMaps.

theorem exists_sum_powQuotSmul (M : ANCModule I n c)
    (φ : resModule I n M.1 →ₗ[A] powQuot I n n) {g f e k : ℕ}
    (hgf : g + c = f) (hk : max S.d 1 = k + 1) (he : f + k * c = e) (hen : e + 2 * c = n)
    (hq : S.q₀ ≤ f) (σ' : S.H M.dual 0 (e : ℤ))
    (hσ : S.ev M e (hq.trans (Nat.le.intro he)) σ' =
      (powQuotLe I (Nat.le.intro hen)).comp φ) :
    ∃ (N : ℕ) (a : Fin N → A) (ha : ∀ i, a i ∈ I ^ c)
      (ψ : Fin N → (resModule I n M.1 →ₗ[A] powQuot I g n)),
      (powQuotLe I ((Nat.le.intro he).trans (Nat.le.intro hen))).comp φ =
        ∑ i, (powQuotSmul I (ha i) hgf).comp (ψ i)

Stacks.LocalCohomology.UniformityIII.exists_sum_powQuotSmul_blowup, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityIII/DivisibleMapsBlowup.lean, line 66.

Let A be a Noetherian ring, I ⊆ A an ideal, q₀ = q(S) and d = d(S) the integers attached to the blowing up of Spec(A) in I (qS I and fibreDim I), M an (A, n, c)-module and φ : M → Iⁿ/I^{2n} an A-linear map. If n ≥ q₀ + (1 + d)c and n ≥ (2 + d)c, then the composition M → Iⁿ/I^{2n} → I^{n-(1+d)c}/I^{2n-(1+d)c} is of the form ∑ aᵢψᵢ with aᵢ ∈ I^c and ψᵢ : M → I^{n-(2+d)c}/I^{2n-(2+d)c}. No hypothesis n ≥ q₀ + 2c is imposed when d = 0.

theorem exists_sum_powQuotSmul_blowup {n c : ℕ} (M : ANCModule I n c)
    (φ : resModule I n M.1 →ₗ[A] powQuot I n n)
    (hn₁ : qS I + (1 + fibreDim I) * c ≤ n) (hn₂ : (2 + fibreDim I) * c ≤ n) :
    ∃ (N : ℕ) (a : Fin N → A) (ha : ∀ i, a i ∈ I ^ c)
      (ψ : Fin N → (resModule I n M.1 →ₗ[A] powQuot I (n - (2 + fibreDim I) * c) n)),
      (powQuotLe I (Nat.sub_le n ((1 + fibreDim I) * c))).comp φ =
        ∑ i, (powQuotSmul I (ha i) (show n - (2 + fibreDim I) * c + c =
          n - (1 + fibreDim I) * c by
            have := two_add_mul_eq (fibreDim I) c; omega)).comp (ψ i)

Tag 0GAD, a lemma

Tag 0GAD in the Stacks Project.

Stacks.LocalCohomology.UniformityIII.ext_one_powQuot_map_eq_zero_blowup, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/LocalCohomology/BitUniformityIII/TwoTermExtBoundBlowup.lean, line 84.

Let A be a Noetherian ring, I ⊆ A an ideal, and q₀ = q(S), d = d(S) the integers attached to the blowing up of Spec(A) in I (qS I and fibreDim I). Let c ≥ 0 and n ≥ q₀ + (1 + d)c, and let K be an object of D(A/Iⁿ) with Hⁱ(K) = 0 for i ≠ -1, 0, with H⁻¹(K) and H⁰(K) finite, and such that Ext¹_{A/Iⁿ}(K, N) is annihilated by I^c for every finite A/Iⁿ-module N. Then the map

Ext¹_{A/Iⁿ}(K, Iⁿ/I^{2n}) ⟶ Ext¹_{A/Iⁿ}(K, I^{n-(1+d)c}/I^{2n-2(1+d)c})

induced by the canonical map of coefficients is zero.

The target is written powQuot I f f = I^f/I^{f+f} with f = n - (1 + d)c, as an A/Iⁿ-module (powQuotObjOfLe); the map is the one induced by Iⁿ ⊆ I^f (powQuotToOfLe).

theorem ext_one_powQuot_map_eq_zero_blowup {n c : ℕ}
    (hn : qS I + (1 + fibreDim I) * c ≤ n)
    (K : DerivedCategory (ModuleCat.{u} (A ⧸ I ^ n)))
    (hK : ∀ i : ℤ, i ≠ -1 → i ≠ 0 →
      IsZero ((DerivedCategory.homologyFunctor (ModuleCat.{u} (A ⧸ I ^ n)) i).obj K))
    (hfin₁ : Module.Finite (A ⧸ I ^ n)
      ((DerivedCategory.homologyFunctor (ModuleCat.{u} (A ⧸ I ^ n)) (-1)).obj K))
    (hfin₀ : Module.Finite (A ⧸ I ^ n)
      ((DerivedCategory.homologyFunctor (ModuleCat.{u} (A ⧸ I ^ n)) 0).obj K))
    (hann : ∀ (N : ModuleCat.{u} (A ⧸ I ^ n)), Module.Finite (A ⧸ I ^ n) N →
      ∀ a ∈ Ideal.map (Ideal.Quotient.mk (I ^ n)) (I ^ c),
      ∀ ξ : DerivedCategory.Ext K
        ((DerivedCategory.singleFunctor (ModuleCat.{u} (A ⧸ I ^ n)) 0).obj N) 1, a • ξ = 0)
    (ξ : DerivedCategory.Ext K
      ((DerivedCategory.singleFunctor (ModuleCat.{u} (A ⧸ I ^ n)) 0).obj (powQuotObj I n n)) 1) :
    ξ ≫ (CategoryTheory.shiftFunctor (DerivedCategory (ModuleCat.{u} (A ⧸ I ^ n))) (1 : ℤ)).map
        ((DerivedCategory.singleFunctor (ModuleCat.{u} (A ⧸ I ^ n)) 0).map
          (powQuotToOfLe I (Nat.sub_le n ((1 + fibreDim I) * c)) (by omega)
            (Nat.sub_le n ((1 + fibreDim I) * c)))) = 0

Sources

• Section 51.22, Tag 0GA6
• AxiomMath/Stacks at 5ed82d14

LeanAssociatedGraded.dInvariant · AssociatedGraded.qInvariant · Stacks.LocalCohomology.UniformityIII.blowupHmod_of_qS_le · AlgebraicGeometry.exceptionalIdeal_pow_le_annihilator_kernel · AlgebraicGeometry.schemeTheoreticSupport_iff_exceptionalTwistContraction_eq_zero · Stacks.LocalCohomology.UniformityIII.ModuleSituation.subsingleton_H_top · Stacks.LocalCohomology.UniformityIII.ModuleSituation.subsingleton_H_next · Stacks.LocalCohomology.UniformityIII.TwistedModuleSituation.Htr_eq_zero

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.