30.17 Ample invertible sheaves… to 30.28 Grothendieck's…

Section30.17 Ample invertible sheaves and cohomology#

Section 30.17 of the Stacks Project, Tag 01XO. 8 tags here are carried by 20 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0B5U, a lemma

Tag 0B5U in the Stacks Project.

AlgebraicGeometry.Scheme.Modules.hasEventualTwistCohomologyVanishing_of_isAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleDegreeCriterion/CohomologicalCriterion.lean, line 148. The attribute's comment: “the implication (1) ⟹ (2)”.

The implication (1) ⟹ (2) of [Stacks, Tag 0B5U], at the tag's own hypotheses: R Noetherian, f : X ⟶ Spec R proper, 𝓛 ample.

This is clause (4) of [Stacks, Tag 0B5T], Stacks.AlgebraicGeometry.ProperAmpleCohomology.exists_isZero_Hgroup_tensorPowTwist, read through the two comparisons of the implementation notes: ampleness is carried across by Stacks.PowerFamilyBridge.isAmple_of_modulesIsAmple and the conclusion by isZero_rightDerived_moduleGlobalSections_of_isZero_Hgroup.

public theorem hasEventualTwistCohomologyVanishing_of_isAmple {R : Type u} [CommRing R]
    [IsNoetherianRing R] (f : X ⟶ Spec (.of R)) [IsProper f] (hL : IsAmple X L) :
    HasEventualTwistCohomologyVanishing L

AlgebraicGeometry.Scheme.Modules.hasIdealTwistH1Vanishing_of_eventualTwistVanishing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleDegreeCriterion/CohomologicalCriterion.lean, line 166. The attribute's comment: “the implication (2) ⟹ (3)”.

The implication (2) ⟹ (3) of [Stacks, Tag 0B5U], on a locally Noetherian scheme and with none of the tag's remaining hypotheses.

A quasi-coherent sheaf of ideals is a quasi-coherent submodule of the structure sheaf, which on a locally Noetherian scheme is coherent ([Stacks, Tag 01Y1], the structure sheaf itself being coherent); condition (2) then applies to it, and is read at p = 1 and at an exponent at least one.

public theorem hasIdealTwistH1Vanishing_of_eventualTwistVanishing [IsLocallyNoetherian X]
    (h : HasEventualTwistCohomologyVanishing L) : HasIdealTwistH1Vanishing L

AlgebraicGeometry.Scheme.Modules.isAmple_of_hasIdealTwistH1Vanishing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleDegreeCriterion/CohomologicalCriterion.lean, line 181. The attribute's comment: “the implication (3) ⟹ (1)”.

The implication (3) ⟹ (1) of [Stacks, Tag 0B5U], on a quasi-compact scheme and with none of the tag's remaining hypotheses. This is [Stacks, Tag 0B5P].

public theorem isAmple_of_hasIdealTwistH1Vanishing [CompactSpace X]
    (h : HasIdealTwistH1Vanishing L) : IsAmple X L

AlgebraicGeometry.Scheme.Modules.isAmple_of_eventualTwistVanishing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleDegreeCriterion/CohomologicalCriterion.lean, line 195. The attribute's comment: “the implication (2) ⟹ (1)”.

The implication (2) ⟹ (1) of [Stacks, Tag 0B5U], at the tag's own hypotheses: R Noetherian, f : X ⟶ Spec R proper. Both steps are unconditional; properness and the Noetherian base enter only through IsLocallyNoetherian X and CompactSpace X.

public theorem isAmple_of_eventualTwistVanishing {R : Type u} [CommRing R] [IsNoetherianRing R]
    (f : X ⟶ Spec (.of R)) [IsProper f] (h : HasEventualTwistCohomologyVanishing L) :
    IsAmple X L

AlgebraicGeometry.Scheme.Modules.tfae_isAmple_twistCohomologyVanishing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleDegreeCriterion/CohomologicalCriterion.lean, line 212. The attribute's comment: “the three equivalent conditions”. References: EGA III (5.2.3), “(ii), special case”.

[Stacks, Tag 0B5U]. For R Noetherian, f : X ⟶ Spec R proper and 𝓛 an invertible 𝒪_X-module, the three conditions

1. 𝓛 is ample;
2. the higher cohomology of ℱ ⊗ 𝓛^{⊗ n} vanishes for every coherent ℱ and all large n;
3. H¹(X, ℐ ⊗ 𝓛^{⊗ n}) = 0 for some n ≥ 1, for every quasi-coherent sheaf of ideals ℐ

are equivalent. The implication (1) ⟹ (2) is clause (4) of [Stacks, Tag 0B5T]; the other two are proved with none of the tag's hypotheses.

public theorem tfae_isAmple_twistCohomologyVanishing {R : Type u} [CommRing R]
    [IsNoetherianRing R] (f : X ⟶ Spec (.of R)) [IsProper f] :
    List.TFAE
      [IsAmple X L, HasEventualTwistCohomologyVanishing L, HasIdealTwistH1Vanishing L]

Tag 0B5V, a lemma

Tag 0B5V in the Stacks Project.

Stacks.AmpleFiniteSurjective.isAmple_modulePullback_of_isFinite_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleFiniteSurjective/Basic.lean, line 278. The attribute's comment: “the implication L ample ⟹ f^* L ample”.

The forward half of [Stacks, Tag 0B5V], at the source's hypothesis list: X proper over a Noetherian ring R, f finite and surjective. The hypotheses other than finiteness are inert; Stacks.AmpleFiniteSurjective.isAmple_modulePullback_of_isFinite is the same statement without them.

theorem isAmple_modulePullback_of_isFinite_surjective (R : Type u) [CommRing R]
    [IsNoetherianRing R] (p : X ⟶ Spec (.of R)) [IsProper p] [IsFinite f] [Surjective f]
    (hL : IsAmple X L) :
    IsAmple Y ((modulePullback f.toLRSHom.toShHom).obj L)

Stacks.AmpleFiniteSurjective.isAmple_iff_isAmple_modulePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleFiniteSurjective/Basic.lean, line 663.

[Stacks, Tag 0B5V]. Let R be a Noetherian ring, let f : Y ⟶ X be a morphism of schemes proper over R — X through p and Y through f ≫ p, which is automatic since a finite morphism is proper and properness composes — and let L be an invertible 𝒪_X-module. If f is finite and surjective, then L is ample if and only if f^* L is ample.

Every binder is the source's: the Noetherian ring, properness over it, finiteness and surjectivity of f, and invertibility of L. ⟹ is isAmple_modulePullback_of_isFinite, which needs only finiteness; ⟸ is isAmple_of_isAmple_modulePullback, the source's cohomological argument.

theorem isAmple_iff_isAmple_modulePullback (R : Type u) [CommRing R] [IsNoetherianRing R]
    (p : X ⟶ Spec (.of R)) [IsProper p] [IsFinite f] [Surjective f] :
    IsAmple X L ↔ IsAmple Y ((modulePullback f.toLRSHom.toShHom).obj L)

Tag 09MR, a lemma

Tag 09MR in the Stacks Project.

Stacks.Cohomology.TwistedLocalizationMap.bijective_canonicalMap_of_le_nonvanishingOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TwistedCohomologyLocalization/CanonicalMap.lean, line 391. The attribute's comment: “for an open U inside the nonvanishing locus X_s: the canonical map H^p_*(U,L,F)_(s) to H^p(U ∩ X_s,F), xi/s^n to s^(-n) xi, is bijective, on an arbitrary scheme, for an arbitrary module and in every degree. The quasi-compact quasi-separated case of the tag is bijective_canonicalMap_of_isCompact, and neither case subsumes the other.”.

The comparison map is bijective on an open contained in the nonvanishing open of s. Let X be a scheme, ℒ an invertible 𝒪_X-module, s a global section of ℒ, ℱ an arbitrary 𝒪_X-module, p a cohomological degree and U ⊆ X_s an open contained in the nonvanishing locus of s. Then the canonical map

H^p_*(U, ℒ, ℱ)₍s₎ ⟶ H^p(U ∩ X_s, ℱ), ξ / sⁿ ↦ s^{-n} ξ

of Stacks.Cohomology.TwistedLocalizationMap.canonicalMap is bijective.

Neither quasi-compactness nor quasi-separatedness of U, nor quasi-coherence of ℱ, nor positivity of p is assumed, and this is not a both-sides-vanish statement: taking U = X_s it reads H^p_*(X_s, ℒ, ℱ)₍s₎ ≅ H^p(X_s, ℱ) on an arbitrary scheme, with neither side forced to be zero.

theorem bijective_canonicalMap_of_le_nonvanishingOpen (hU : U ≤ nonvanishingOpen L s) :
    Function.Bijective (canonicalMap X L s F p U)

Stacks.Cohomology.TwistedLocalizationMap.bijective_canonicalMap_of_isCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TwistedCohomologyLocalization/MayerVietorisStep.lean, line 981.

[Stacks, Tag 09MR] over a quasi-compact open of a quasi-separated scheme. For a quasi-compact open S of a quasi-separated scheme X, an invertible 𝒪_X-module ℒ, a global section s of ℒ, a quasi-coherent 𝒪_X-module ℱ and any degree p, the comparison map

H^p_*(S, ℒ, ℱ)₍s₎ ⟶ H^p(S ∩ X_s, ℱ), ξ / sⁿ ↦ s^{-n} ξ

is bijective.

theorem bijective_canonicalMap_of_isCompact [QuasiSeparatedSpace X]
    (S : X.Opens) (hS : IsCompact (S : Set X)) (p : ℕ) :
    Function.Bijective (canonicalMap X L s F p S)

Stacks.Cohomology.TwistedLocalizationMap.bijective_canonicalMap_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/TwistedCohomologyLocalization/MayerVietorisStep.lean, line 990.

[Stacks, Tag 09MR] on a quasi-compact quasi-separated scheme.

theorem bijective_canonicalMap_top [QuasiSeparatedSpace X] [CompactSpace X] (p : ℕ) :
    Function.Bijective (canonicalMap X L s F p ⊤)

Tag 01XR, a lemma

Tag 01XR in the Stacks Project.

Stacks.SheafOfModules.exists_sectionPowerAction_eq_zero_of_isAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionPowerCohomology/Basic.lean, line 123. The attribute's comment: “the case of an affine ambient scheme”.

The conclusion of [Stacks, Tag 01XR] for an affine ambient scheme. On an affine scheme the positive-degree cohomology of a quasi-coherent module vanishes, so every class is annihilated already by the zeroth power of a global section of an invertible module.

theorem exists_sectionPowerAction_eq_zero_of_isAffine [IsAffine X] (s : L.sections)
    [CompactSpace X] [QuasiSeparatedSpace X] (_hU : IsAffineOpen (nonvanishingOpen L s))
    (F : X.Modules) [F.IsQuasicoherent] (p : ℕ) (hp : 0 < p)
    (ξ : Hgroup X.ringCatSheaf ⊤ p F) :
    ∃ (n : ℕ) (t : SheafOfModules.unit X.ringCatSheaf ⟶
        TensorPower.tensorPower X.toRingedSpace.presheaf
          (structureSheafRing X.toRingedSpace).property L n),
      IsSectionPowerHom X.toRingedSpace.presheaf
          (structureSheafRing X.toRingedSpace).property L s n t ∧
        (Hfunctor X.ringCatSheaf ⊤ p).map
          (sectionPowerAction X.toRingedSpace.presheaf
            (structureSheafRing X.toRingedSpace).property L F n t) ξ = 0

Stacks.SheafOfModules.exists_sectionPowerAction_eq_zero_of_finite_affine_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionPowerCohomology/Basic.lean, line 144. The attribute's comment: “the degrees at least the size of a finite affine cover”.

The conclusion of [Stacks, Tag 01XR] above the size of a finite affine cover. On a scheme with affine diagonal covered by t affine opens the cohomology of a quasi-coherent module vanishes in every degree at least t, so in those degrees every class is annihilated already by the zeroth power of a global section of an invertible module.

theorem exists_sectionPowerAction_eq_zero_of_finite_affine_cover
    [IsAffineHom (pullback.diagonal (terminal.from X))] (s : L.sections)
    [CompactSpace X] [QuasiSeparatedSpace X] (_hU : IsAffineOpen (nonvanishingOpen L s))
    {t : ℕ} (U : Fin t → X.Opens) (hUaff : ∀ i, IsAffineOpen (U i)) (hUcover : ⨆ i, U i = ⊤)
    (F : X.Modules) [F.IsQuasicoherent] (p : ℕ) (_hp : 0 < p) (ht : t ≤ p)
    (ξ : Hgroup X.ringCatSheaf ⊤ p F) :
    ∃ (n : ℕ) (t' : SheafOfModules.unit X.ringCatSheaf ⟶
        TensorPower.tensorPower X.toRingedSpace.presheaf
          (structureSheafRing X.toRingedSpace).property L n),
      IsSectionPowerHom X.toRingedSpace.presheaf
          (structureSheafRing X.toRingedSpace).property L s n t' ∧
        (Hfunctor X.ringCatSheaf ⊤ p).map
          (sectionPowerAction X.toRingedSpace.presheaf
            (structureSheafRing X.toRingedSpace).property L F n t') ξ = 0

Stacks.SheafOfModules.exists_sectionPowerAction_eq_zero_of_isAffineOpen_nonvanishingOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionPowerCohomology/Localization.lean, line 152.

[Stacks, Tag 01XR]. Let X be a quasi-compact quasi-separated scheme, ℒ an invertible 𝒪_X-module and s ∈ Γ(X, ℒ) a global section whose nonvanishing open X_s is affine. Then every cohomology class of a quasi-coherent 𝒪_X-module in a positive degree is annihilated by some power of s.

This is the general case; ./Basic.lean has the two cases in which the cohomology group itself vanishes. The conclusion quantifies over the morphisms 𝒪_X ⟶ ℒ^{⊗ k} representing s^k, as those statements do, and is witnessed by the canonical representative Stacks.SheafOfModules.sectionPowerHom.

theorem exists_sectionPowerAction_eq_zero_of_isAffineOpen_nonvanishingOpen [CompactSpace X]
    [QuasiSeparatedSpace X] (hU : IsAffineOpen (nonvanishingOpen L s)) (p : ℕ) (hp : 0 < p)
    (ξ : (Hgroup X.ringCatSheaf ⊤ p F : Type u)) :
    ∃ (n : ℕ) (t : SheafOfModules.unit X.ringCatSheaf ⟶
        TensorPower.tensorPower X.toRingedSpace.presheaf
          (structureSheafRing X.toRingedSpace).property L n),
      IsSectionPowerHom X.toRingedSpace.presheaf
          (structureSheafRing X.toRingedSpace).property L s n t ∧
        (Hfunctor X.ringCatSheaf ⊤ p).map
          (sectionPowerAction X.toRingedSpace.presheaf
            (structureSheafRing X.toRingedSpace).property L F n t) ξ = 0

Stacks.SheafOfModules.exists_sectionPowerAction_eq_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/SectionPowerCohomology/QuasiCompact.lean, line 141.

[Stacks, Tag 01XR]. Let X be a scheme, ℒ an invertible 𝒪_X-module and s ∈ Γ(X, ℒ) a global section. If X is quasi-compact and quasi-separated and X_s is affine, then for every quasi-coherent 𝒪_X-module ℱ, every p > 0 and every ξ ∈ Hᵖ(X, ℱ) there is n ≥ 0 with sⁿ ξ = 0 in Hᵖ(X, ℱ ⊗ ℒ^{⊗ n}).

Multiplication by sⁿ is Stacks.SheafOfModules.sectionPowerAction along the morphism t : 𝒪_X ⟶ ℒ^{⊗ n} representing sⁿ (Stacks.SheafOfModules.IsSectionPowerHom; such a t is unique, by Stacks.SheafOfModules.IsSectionPowerHom.unique, and exists, by Stacks.SheafOfModules.isSectionPowerHom_sectionPowerHom).

theorem exists_sectionPowerAction_eq_zero (X : Scheme.{u})
    (L : SheafOfModules.{u} (structureSheafRing X.toRingedSpace))
    [IsInvertible X.toRingedSpace.presheaf (structureSheafRing X.toRingedSpace).property L]
    [CompactSpace X] [QuasiSeparatedSpace X] (s : L.sections)
    (hU : IsAffineOpen (nonvanishingOpen L s)) (F : X.Modules) [F.IsQuasicoherent] (p : ℕ)
    (hp : 0 < p) (ξ : Hgroup X.ringCatSheaf ⊤ p F) :
    ∃ n : ℕ, ∀ (t : SheafOfModules.unit X.ringCatSheaf ⟶
        TensorPower.tensorPower X.toRingedSpace.presheaf
          (structureSheafRing X.toRingedSpace).property L n),
      IsSectionPowerHom X.toRingedSpace.presheaf
          (structureSheafRing X.toRingedSpace).property L s n t →
        (Hfunctor X.ringCatSheaf ⊤ p).map
          (sectionPowerAction X.toRingedSpace.presheaf
            (structureSheafRing X.toRingedSpace).property L F n t) ξ = 0

Tag 09MS, a lemma

Tag 09MS in the Stacks Project.

Stacks.AmpleSurjectiveThickening.isAmple_modulePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleSurjectiveThickening/Basic.lean, line 107. The attribute's comment: “the implication L ample ⟹ i^* L ample”.

L ample ⟹ i^* L ample. For a closed immersion i : Z ⟶ X of Noetherian schemes inducing a homeomorphism of underlying spaces, ampleness of an invertible 𝒪_X-module L gives ampleness of i^* L ([Stacks, Tag 0892]). The proof is Stacks.AmpleClosedImmersion.isAmple_modulePullback_of_surjective_isClosedImmersion.

theorem isAmple_modulePullback [IsClosedImmersion i] [Surjective i] [IsNoetherian X]
    (hL : IsAmple X L) :
    IsAmple Z ((modulePullback i.toLRSHom.toShHom).obj L)

Stacks.AmpleSurjectiveThickening.isAmple_modulePullback_iff_isAmple_of_isHomeomorph, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleSurjectiveThickening/Basic.lean, line 254.

[Stacks, Tag 09MS]. Let i : Z ⟶ X be a closed immersion of Noetherian schemes inducing a homeomorphism of underlying topological spaces, and let L be an invertible 𝒪_X-module. Then i^* L is ample on Z if and only if L is ample on X. Noetherianness of Z follows from that of X, since i is a closed immersion, and is not assumed.

theorem isAmple_modulePullback_iff_isAmple_of_isHomeomorph [IsClosedImmersion i] [IsNoetherian X]
    (hi : IsHomeomorph i.base) :
    IsAmple Z ((modulePullback i.toLRSHom.toShHom).obj L) ↔ IsAmple X L

Tag 0B7K, a lemma

Tag 0B7K in the Stacks Project.

Stacks.AmpleSurjectiveThickening.isQuasiAffine_iff_isQuasiAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleSurjectiveThickening/QuasiAffine.lean, line 145.

[Stacks, Tag 0B7K]. Let i : Z ⟶ X be a closed immersion of Noetherian schemes inducing a homeomorphism of underlying topological spaces — that is, a closed immersion surjective on points. Then X is quasi-affine if and only if Z is quasi-affine.

theorem isQuasiAffine_iff_isQuasiAffine [IsClosedImmersion i] [Surjective i] [IsNoetherian X] :
    X.IsQuasiAffine ↔ Z.IsQuasiAffine

Stacks.Thickenings.isQuasiAffine_iff_of_isNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/MoreMorphisms/ThickeningMorphism/QuasiAffineAscent.lean, line 550. References: EGA II (5.1.10), “(vi), special case”.

[Stacks Project, Tag 0B7K]. For a closed immersion i : Z ⟶ X of Noetherian schemes inducing a homeomorphism of underlying spaces — equivalently, a surjective closed immersion — the ambient scheme is quasi-affine if and only if the closed subscheme is.

Both implications are unconditional. Ambient ⟹ closed subscheme is the elementary one, a closed immersion being affine (Stacks.Thickenings.isQuasiAffine_of_isQuasiAffine_ambient). Closed subscheme ⟹ ambient is Stacks.Thickenings.isQuasiAffine_of_isThickening_of_isLocallyNoetherian: over a Noetherian scheme a thickening is of finite order, and along a finite-order thickening an affine basic open lifts, by the square-zero computation of Stacks.Thickenings.affineBasicOpenLifts_of_isFirstOrderThickening_of_isQuasiAffine along the filtration by the powers of the ideal sheaf. Neither the ampleness criterion [Stacks Project, Tag 01QE] nor [Stacks Project, Tag 09MS] nor any cohomology group enters, so the hypothesis Stacks.AmpleClosedImmersion.SectionsLiftAfterPower carried by Stacks.AmpleSurjectiveThickening.isQuasiAffine_iff_of_sectionsLiftAfterPower is discharged.

Noetherianness of the closed subscheme is not used, and of the ambient scheme only local Noetherianness together with quasi-compactness; both are carried because the source assumes them.

theorem isQuasiAffine_iff_of_isNoetherian {Z X : Scheme.{u}} (i : Z ⟶ X) [IsClosedImmersion i]
    [Surjective i] [IsNoetherian Z] [IsNoetherian X] :
    X.IsQuasiAffine ↔ Z.IsQuasiAffine

Tag 0EBD, a lemma

Tag 0EBD in the Stacks Project.

Stacks.AlgebraicGeometry.CohomologyColimitReduction.isAffine_of_isZero_cohomology_negative_tensorPower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CohomologyColimitReduction/Basic.lean, line 258.

[Stacks, Tag 0EBD]. Let L be an ample invertible module on a scheme X and let n₀ be an integer such that Hᵖ(X, L^{⊗ -n}) = 0 for every n ≥ n₀ and every p > 0. Then X is affine.

Everything the dévissage of the tag needs beyond this hypothesis comes from ampleness itself: quasi-compactness is part of ampleness and quasi-separatedness follows from it ([Stacks, Tag 01PV]), which makes the colimit reduction ([Stacks, Tag 01PG] with [Stacks, Tag 01FF]) available and supplies a degree beyond which the cohomology of every quasi-coherent module vanishes ([Stacks, Tag 071L], in the form AlgebraicGeometry.exists_isZero_hgroup_top); the dévissage sequence presenting a quasi-coherent module of finite type as a quotient of a finite direct sum of negative twists of L is clause (8) of [Stacks, Tag 01Q3]; and the vanishing of Hᵖ on all quasi-coherent modules in all positive degrees gives affineness by Serre's criterion ([Stacks, Tag 01XF]).

theorem isAffine_of_isZero_cohomology_negative_tensorPower (L : X.Modules)
    [Stacks.Ample.IsInvertibleModule X L] (hL : Stacks.Ample.IsAmple X L) (n₀ : ℤ)
    (hvan : ∀ (n : ℤ) (p : ℕ), n₀ ≤ n → 0 < p →
      IsZero (Hgroup X.ringCatSheaf ⊤ p (Stacks.Ample.tensorPowModule X L (-n)))) :
    IsAffine X

Tag 0EBE, a lemma

Tag 0EBE in the Stacks Project.

Stacks.AlgebraicGeometry.CohomologyColimitReduction.isAffine_of_isZero_hgroup_unitModule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/CohomologyColimitReduction/QuasiAffine.lean, line 102.

[Stacks, Tag 0EBE]. Let X be a quasi-affine scheme. If Hᵖ(X, 𝒪_X) = 0 for every p > 0, then X is affine.

The source's argument verbatim: 𝒪_X is an ample invertible module on a quasi-affine scheme ([Stacks, Tag 01QE], Stacks.Ample.isAmple_unitModule_of_isQuasiAffine), so affineness follows from the vanishing of the higher cohomology of the negative twists of an ample module ([Stacks, Tag 0EBD], isAffine_of_isZero_cohomology_negative_tensorPower). Tag 0EBD's family of hypotheses collapses to this single one because the twists of 𝒪_X are all 𝒪_X, by isZero_hgroup_tensorPowModule_unitModule; the threshold n₀ is taken to be 0 and is immaterial.

theorem isAffine_of_isZero_hgroup_unitModule (X : Scheme.{u}) [X.IsQuasiAffine]
    (hvan : ∀ p : ℕ, 0 < p →
      IsZero (Hgroup X.ringCatSheaf ⊤ p (SheafOfModules.unit X.ringCatSheaf))) :
    IsAffine X

Sources

• Section 30.17, Tag 01XO
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.Scheme.Modules.hasEventualTwistCohomologyVanishing_of_isAmple · AlgebraicGeometry.Scheme.Modules.hasIdealTwistH1Vanishing_of_eventualTwistVanishing · AlgebraicGeometry.Scheme.Modules.isAmple_of_hasIdealTwistH1Vanishing · AlgebraicGeometry.Scheme.Modules.isAmple_of_eventualTwistVanishing · AlgebraicGeometry.Scheme.Modules.tfae_isAmple_twistCohomologyVanishing · Stacks.AmpleFiniteSurjective.isAmple_modulePullback_of_isFinite_surjective · Stacks.AmpleFiniteSurjective.isAmple_iff_isAmple_modulePullback · Stacks.Cohomology.TwistedLocalizationMap.bijective_canonicalMap_of_le_nonvanishingOpen

Section30.18 Chow's Lemma#

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

Tag 0200, a lemma

Tag 0200 in the Stacks Project.

AlgebraicGeometry.hasDenseChowModification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Segre/ChartSurjective.lean, line 415. References: EGA II (5.6.1), “(a); (i),(ii)”; SGA 4 XVII (7.0.6), “Noetherian base”; SGA 4 XII (7.1), “Noetherian case”; SGA 4½ Arcata (3.4.3), “Chow's lemma step”.

Chow's lemma over a Noetherian base.

theorem hasDenseChowModification {X S : Scheme.{u}} (f : X ⟶ S) [IsNoetherian S]
    [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f] :
    HasDenseChowModification f

Tag 0201, a remark

Tag 0201 in the Stacks Project.

AlgebraicGeometry.isClosedImmersion_chowGraph, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ChowNoetherian/Refinements.lean, line 107. The attribute's comment: “part (1): X' ⟶ 𝐏ⁿ_S ×_S X = 𝐏ⁿ_X is a closed immersion”.

The graph of a proper modification is a closed immersion. It is proper, because the projection 𝐏ⁿ_S ×_S X ⟶ X is separated and the composite is π, and a monomorphism, because the composite with the projection to 𝐏ⁿ_S is the immersion i.

theorem isClosedImmersion_chowGraph (π : X' ⟶ X) (i : X' ⟶ ProjectiveSpace n S) [IsProper π]
    [IsImmersion i] (hcomm : π ≫ f = i ≫ (ProjectiveSpace n S ↘ S)) :
    IsClosedImmersion (chowGraph π i hcomm)

AlgebraicGeometry.isProjectiveMorphism_chowModification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ChowNoetherian/Refinements.lean, line 130. The attribute's comment: “part (1): π is H-projective”.

The modification in Chow's lemma is H-projective. Its graph is a closed immersion into the projective space 𝐏ⁿ_X over X, compatibly with the structure morphism.

theorem isProjectiveMorphism_chowModification (π : X' ⟶ X) (i : X' ⟶ ProjectiveSpace n S)
    [IsProper π] [IsImmersion i] (hcomm : π ≫ f = i ≫ (ProjectiveSpace n S ↘ S)) :
    IsProjectiveMorphism π

AlgebraicGeometry.isProjective_chowModification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ChowNoetherian/Refinements.lean, line 137. The attribute's comment: “part (1): π is projective”.

The modification in Chow's lemma is projective: an H-projective morphism is projective.

theorem isProjective_chowModification (π : X' ⟶ X) (i : X' ⟶ ProjectiveSpace n S) [IsProper π]
    [IsImmersion i] (hcomm : π ≫ f = i ≫ (ProjectiveSpace n S ↘ S)) :
    IsProjective π

AlgebraicGeometry.exists_isSchemeTheoreticallyDense_chowModification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ChowNoetherian/Refinements.lean, line 187. The attribute's comment: “part (2): π⁻¹(U) may be assumed scheme-theoretically dense in X'”. References: EGA II (5.6.2), “f⁻¹(U) dense in X'”.

In Chow's lemma the inverse image of the dense open may be assumed scheme-theoretically dense. Replace X' by the scheme-theoretic closure of π⁻¹(U); the dimension n of the ambient projective space and the dense open U are unchanged.

theorem exists_isSchemeTheoreticallyDense_chowModification (f : X ⟶ S) [IsNoetherian S]
    [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f] (π : X' ⟶ X)
    (i : X' ⟶ ProjectiveSpace n S) (U : X.Opens) [IsProper π] [IsImmersion i]
    (hcomm : π ≫ f = i ≫ (ProjectiveSpace n S ↘ S)) (hU : Dense (U : Set X))
    (hiso : IsIso (π ∣_ U)) :
    ∃ (Y : Scheme.{u}) (ρ : Y ⟶ X) (j : Y ⟶ ProjectiveSpace n S),
      IsProper ρ ∧ Surjective ρ ∧ IsImmersion j ∧
        ρ ≫ f = j ≫ (ProjectiveSpace n S ↘ S) ∧ Dense (U : Set X) ∧ IsIso (ρ ∣_ U) ∧
        Scheme.Opens.IsSchemeTheoreticallyDense (ρ ⁻¹ᵁ U)

AlgebraicGeometry.exists_isReduced_chowModification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ChowNoetherian/Refinements.lean, line 207. The attribute's comment: “part (3): if X is reduced then X' may be chosen reduced”. References: EGA II (5.6.2), “reduced X' clause”.

In Chow's lemma over a reduced scheme the modification may be chosen reduced. The scheme-theoretic closure of π⁻¹(U) has reduced source, since π⁻¹(U) ≅ U is an open subscheme of the reduced scheme X, and the scheme-theoretic image of a reduced scheme is reduced.

theorem exists_isReduced_chowModification (f : X ⟶ S) [IsNoetherian S] [IsSeparated f]
    [LocallyOfFiniteType f] [QuasiCompact f] [IsReduced X] (π : X' ⟶ X)
    (i : X' ⟶ ProjectiveSpace n S) (U : X.Opens) [IsProper π] [IsImmersion i]
    (hcomm : π ≫ f = i ≫ (ProjectiveSpace n S ↘ S)) (hU : Dense (U : Set X))
    (hiso : IsIso (π ∣_ U)) :
    ∃ (Y : Scheme.{u}) (ρ : Y ⟶ X) (j : Y ⟶ ProjectiveSpace n S),
      IsProper ρ ∧ Surjective ρ ∧ IsImmersion j ∧
        ρ ≫ f = j ≫ (ProjectiveSpace n S ↘ S) ∧ Dense (U : Set X) ∧ IsIso (ρ ∣_ U) ∧
        Scheme.Opens.IsSchemeTheoreticallyDense (ρ ⁻¹ᵁ U) ∧ IsReduced Y

Sources

• Section 30.18, Tag 02O2
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.hasDenseChowModification · AlgebraicGeometry.isClosedImmersion_chowGraph · AlgebraicGeometry.isProjectiveMorphism_chowModification · AlgebraicGeometry.isProjective_chowModification · AlgebraicGeometry.exists_isSchemeTheoreticallyDense_chowModification · AlgebraicGeometry.exists_isReduced_chowModification

Section30.19 Higher direct images of coherent sheaves#

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

Tag 02O5, a proposition

Tag 02O5 in the Stacks Project.

AlgebraicGeometry.ProperCoherenceWitness.higherDirectImageIsCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProperCoherenceWitness/ChowStalk.lean, line 202.

Coherence of higher direct images. Let S be a locally Noetherian scheme, let f : X ⟶ S be proper and let F be a coherent 𝒪_X-module. Then R ⁱ f_* F is a coherent 𝒪_S-module for every i ≥ 0.

theorem higherDirectImageIsCoherent : HigherDirectImageIsCoherent.{u}

AlgebraicGeometry.ProperCoherenceWitness.isCoherent_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProperCoherenceWitness/ChowStalk.lean, line 213. References: EGA III (2.2.5), “partial”.

Coherence of the direct image. For f : X ⟶ S proper onto a locally Noetherian base and F coherent, f_* F is coherent.

theorem isCoherent_pushforward {X S : Scheme.{u}} (f : X ⟶ S) [IsLocallyNoetherian S]
    [IsProper f] (F : X.Modules) [F.IsCoherent] :
    ((Scheme.Modules.pushforward f).obj F).IsCoherent

Tag 02O6, a lemma

Tag 02O6 in the Stacks Project.

AlgebraicGeometry.ProperCoherenceWitness.moduleFinite_cohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProperCoherenceWitness/ChowStalk.lean, line 223. References: EGA III (3.2.3).

Finiteness of cohomology. Let S = Spec A with A Noetherian, let f : X ⟶ S be proper and let F be a coherent 𝒪_X-module. Then Hⁱ(X, F) is a finite A-module for every i ≥ 0. Here the base is an affine locally Noetherian scheme and A is its ring of global sections.

theorem moduleFinite_cohomology {X S : Scheme.{u}} (f : X ⟶ S) [IsProper f] [IsAffine S]
    [IsLocallyNoetherian S] (F : X.Modules) [F.IsCoherent] (i : ℕ) :
    Module.Finite Γ(S, ⊤) ((ModuleCat.restrictScalars f.appTop.hom).obj
      (((moduleGlobalSections X).rightDerived i).obj F))

Tag 0897, a lemma

Tag 0897 in the Stacks Project.

Stacks.AlgebraicGeometry.GradedProperCohomology.exists_isZero_pieceTwistCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GradedProperCohomology/Basic.lean, line 232. The attribute's comment: “part (2), with the base change X' = Spec(B) ×_Spec(A) X and the comparison of the vanishing of H^p(X', F' tensor (pi^ L)^d) with that of the H^p(X, F_n tensor L^d) (089W, 01E8) as hypotheses; 02O1 enters through its own hypothesis VanishingOverAffineBase, and ampleness of pi^ L is derived from that of L by 0892 and 01VK”.

[Stacks, Tag 0897] part (2), granted the base change and [Stacks, Tag 02O1]'s own hypothesis. Let A be a Noetherian ring, B a finitely generated graded A-algebra, f : X ⟶ Spec A proper, F a quasi-coherent graded 𝓑-module of finite type and L an invertible 𝒪_X-module. Then there is a d₀ such that

H^p(X, Fₙ ⊗ L^{⊗d}) = 0 for every p > 0, every d ≥ d₀ and every graded degree n,

the uniformity in n being the whole point: it is what [Stacks, Tag 0884] consumes.

The hypotheses beyond the source's are the base change of the source's proof — f' : X' ⟶ Spec B proper, the affine projection π : X' ⟶ X, a coherent F' on X', and the comparison hcmp of the vanishing of H^p(X', F' ⊗ (π^* L)^{⊗d}) with that of every H^p(X, Fₙ ⊗ L^{⊗d}), which is [Stacks, Tag 089W] along π together with the projection formula [Stacks, Tag 01E8] — plus hvan, which is [Stacks, Tag 02O1]'s own hypothesis and not an extra one. Ampleness is not assumed upstairs: the source's own hL : IsAmple X L is used, and π^* L is ample on X' because π is affine ([Stacks, Tag 0892] part (2), Stacks.AmplePullback.isAmple_modulePullback_of_isAffineHom), hence ample relative to f' because Spec B is affine ([Stacks, Tag 01VK], Stacks.RelativeAmpleAffineBase.isRelativelyAmple_iff_isAmple).

The uniformity in n is not assumed and is not smuggled in by hcmp: hcmp turns one vanishing statement upstairs into the vanishing of all the graded pieces downstairs, exactly as the single coherent sheaf F' on X' accounts for the whole graded module F. What is proved here is that the bound d₀ exists at all: [Stacks, Tag 02O1] applied to f', F' and π^* L gives a d₀ above which R^p f'_*(F' ⊗ (π^* L)^{⊗d}) vanishes for every p > 0, [Stacks, Tag 01XK] turns that into the vanishing of H^p(X', F' ⊗ (π^* L)^{⊗d}) — Spec B is affine and f', being proper, is quasi-compact and quasi-separated — and hcmp transports it to X.

theorem exists_isZero_pieceTwistCohomology
    (A : Type u) [CommRing A] [IsNoetherianRing A] {B : Type u} [CommRing B] [Algebra A B]
    (𝒜 : ℕ → Submodule A B) [GradedAlgebra 𝒜] [Algebra.FiniteType A B]
    (f : X ⟶ Spec (.of A)) [IsProper f]
    (F : _root_.SheafOfModules.GradedModule 𝓑)
    (_hqc : ∀ n : ℤ, (pieceModule F n).IsQuasicoherent)
    (_hft : Stacks.Coherent.IsFiniteTypeOnAffine F)
    (L : X.Modules) [IsInvertibleModule X L] (hL : IsAmple X L)
    (hvan : Stacks.AlgebraicGeometry.RelativeAmpleTwistVanishing.VanishingOverAffineBase.{u})
    {X' : Scheme.{u}} (f' : X' ⟶ Spec (.of B)) [IsProper f']
    (π : X' ⟶ X) [_root_.AlgebraicGeometry.IsAffineHom π]
    (F' : X'.Modules) [F'.IsCoherent]
    (hcmp : ∀ p d : ℕ,
      IsZero ((ModuleCat.restrictScalars f'.appTop.hom).obj
          (cohomologyOf X' p
            (tensorModules X' F'
              (tensorPowModule X' (Stacks.AmpleLocallyClosed.pullbackModule π L) (d : ℤ))))) →
        ∀ n : ℤ, IsZero (cohomologyOf X p (pieceTwist F L n (d : ℤ)))) :
    ∃ d₀ : ℕ, ∀ d : ℕ, d₀ ≤ d → ∀ p : ℕ, 0 < p → ∀ n : ℤ,
      IsZero (cohomologyOf X p (pieceTwist F L n (d : ℤ)))

Stacks.AlgebraicGeometry.GradedProperCohomology.moduleFinite_gradedCohomologySum_and_exists_isZero_pieceTwistCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GradedProperCohomology/FiniteGradedCohomology.lean, line 220. The attribute's comment: “both parts, at the hypotheses of the source: A Noetherian, B a finitely generated graded A-algebra, f : X → Spec A proper, F a quasi-coherent graded f^* B-tilde-module of finite type, and L ample invertible in part (2)”. References: SGA 2 XII (5.8), “(i), special case”.

[Stacks, Tag 0897]. Let A be a Noetherian ring, B a finitely generated graded A-algebra, f : X ⟶ Spec A a proper morphism and 𝓑 = f^* B̃. Let F be a quasi-coherent graded 𝓑-module of finite type. Then

1. for every p the graded B-module Hᵖ(X, F) = ⨁ₙ Hᵖ(X, Fₙ) is a finite B-module, and
2. if L is an ample invertible 𝒪_X-module there is a d₀ with Hᵖ(X, Fₙ ⊗ L^{⊗d}) = 0 for all p > 0 and all d ≥ d₀, uniformly in the graded degree n.

The B-module structure in (1) is HomogeneousSections.gradedCohomologyModule for the homogeneous-sections datum of 𝓑 = f^* B̃: a homogeneous b ∈ 𝒜ₖ carries the degree-n summand to the degree-n + k summand by Hᵖ(X, −) of multiplication by the global section of 𝓑ₖ that b names.

theorem moduleFinite_gradedCohomologySum_and_exists_isZero_pieceTwistCohomology
    [IsNoetherianRing A] [Algebra.FiniteType A B] [_root_.AlgebraicGeometry.IsProper f]
    (F : _root_.SheafOfModules.GradedModule.{u, u, u} (pullbackGradedAlg 𝒜 f))
    (hqc : ∀ n : ℤ, (pieceModule F n).IsQuasicoherent) (hft : F.IsFiniteType) :
    (letI := (pullbackHomogeneousSections 𝒜 f).gradedCohomologyModule F
     ∀ p : ℕ, Module.Finite B (gradedCohomologySum F p)) ∧
      ∀ (L : X.Modules) (_ : IsInvertibleModule X L), IsAmple X L →
        ∃ d₀ : ℕ, ∀ d : ℕ, d₀ ≤ d → ∀ p : ℕ, 0 < p → ∀ n : ℤ,
          IsZero (cohomologyOf X p (pieceTwist F L n (d : ℤ)))

Stacks.AlgebraicGeometry.GradedProperCohomology.moduleFinite_gradedCohomologySum, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GradedProperCohomology/ProperCohomologyFiniteness.lean, line 104. The attribute's comment: “part (1), with the base change X' = Spec(B) ×_Spec(A) X, the graded B-action on the graded cohomology and its comparison with H^p(X', F') (089W) as hypotheses”.

[Stacks, Tag 0897] part (1), granted the base change. Let A be a Noetherian ring, B a finitely generated graded A-algebra, f : X ⟶ Spec A proper and F a quasi-coherent graded 𝓑-module of finite type. Then the graded B-module ⨁ₙ H^p(X, Fₙ) is a finite B-module, for every p.

The hypotheses beyond the source's are the base change of the source's proof alone: f' : X' ⟶ Spec B proper with a coherent F' on X', the graded B-action on ⨁ₙ H^p(X, Fₙ), and the B-linear comparison cmp with H^p(X', F') that [Stacks, Tag 089W] provides because X' ⟶ X is affine. [Stacks, Tag 02O6] is not assumed: it is tag02O6 above.

"Of finite type" is SheafOfModules.GradedModule.IsFiniteType, the local notion of [Stacks, Tag 03DL] part (5) read for a graded module, which is the source's own hypothesis; it is inert in this implication (finite type of F enters the source's argument only in producing F' and its coherence, which here are binders) and is retained because dropping it would state something other than [Stacks, Tag 0897]. It is also exactly the predicate Stacks.Cohomology.FormalFunctions.isCohomologyReesFinite_of_isCoherent has available when it instantiates this tag for [Stacks, Tag 02O8].

Given the base change, the content is that [Stacks, Tag 02O6] applies to f' with the ring B: B is Noetherian because it is a finitely generated algebra over the Noetherian ring A, and F' is coherent, so H^p(X', F') is a finite B-module and cmp carries that finiteness back to ⨁ₙ H^p(X, Fₙ).

theorem moduleFinite_gradedCohomologySum {X : Scheme.{u}}
    {𝓑 : _root_.SheafOfModules.GradedAlgebra.{u, u} X.ringCatSheaf}
    (A : Type u) [CommRing A] [IsNoetherianRing A] {B : Type u} [CommRing B] [Algebra A B]
    (𝒜 : ℕ → Submodule A B) [_root_.GradedAlgebra 𝒜] [Algebra.FiniteType A B]
    (f : X ⟶ Spec (.of A)) [IsProper f]
    (F : _root_.SheafOfModules.GradedModule 𝓑)
    (_hqc : ∀ n : ℤ, (pieceModule F n).IsQuasicoherent)
    (_hft : F.IsFiniteType)
    (p : ℕ)
    {X' : Scheme.{u}} (f' : X' ⟶ Spec (.of B)) [IsProper f']
    (F' : X'.Modules) [F'.IsCoherent]
    [Module B (gradedCohomologySum F p)]
    (cmp : gradedCohomologySum F p ≃ₗ[B]
      ↥((ModuleCat.restrictScalars (specAlgebraRingHom B f')).obj
        (cohomologyOf X' p F'))) :
    Module.Finite B (gradedCohomologySum F p)

Stacks.AlgebraicGeometry.GradedProperCohomology.moduleFinite_gradedCohomologySum_gradedPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/GradedProperCohomology/ProperCohomologyFinitenessSupplement.lean, line 415. The attribute's comment: “part (1), with the graded algebra read as the source defines it, B = f^* Btilde for Btilde the graded algebra sheaf of B on Spec(A), and over the base change X' = Spec(B) ×_Spec(A) X that the proof builds: the graded B-module ⨁_n H^p(X, F_n) is a finite B-module, for the B-action carried across the comparison of Tag 089W rather than the one the source defines degreewise”.

[Stacks, Tag 0897] part (1), with 𝓑 = f^* B̃ and over the base change the proof constructs. Let A be a Noetherian ring, B a finitely generated graded A-algebra, f : X ⟶ Spec A proper, 𝓑 = f^* B̃, and F a quasi-coherent graded 𝓑-module of finite type. Then the graded B-module ⨁ₙ H^p(X, Fₙ) is a finite B-module, for every p.

The graded algebra 𝓑 is the source's own: B̃ is Stacks.AffineGradedAlgebra.gradedTildeOf A 𝒜, the sheaf of graded 𝒪_{Spec A}-algebras whose degree-n piece is the associated sheaf (𝒜 n)~, and the pullback along f is Stacks.Conormal.gradedPullback.

The base change of the source's proof is built here rather than assumed: baseChangeScheme A B f is X' = Spec(B) ×_{Spec(A)} X and baseChangeToSpec A B f is its structure morphism f' : X' ⟶ Spec B, which is proper because properness is stable under base change in Mathlib. The projection π : X' ⟶ X is pullback.snd, and it is affine for the same reason, which is what makes [Stacks, Tag 089W] applicable to it.

Nothing is carried. The coherent F' on X' and the identification e : π_* F' ≅ ∐ₙ Fₙ of its direct image, which the source's statement does not mention, are produced by exists_isCoherent_pushforward_baseChange_iso_intCoprod above, so the registration is unconditional; the graded B-action on ⨁ₙ H^p(X, Fₙ) and a B-linear comparison with H^p(X', F') are produced from e, by gradedCohomologySumModule.

Where the B-action comes from. It is gradedCohomologySumModuleOfFiniteType, i.e. gradedCohomologySumModule at the produced F' and e: cohomology of a quasi-compact quasi-separated scheme commutes with the ℤ-indexed direct sum (Stacks.AlgebraicGeometry.GradedProperCohomology.cohomologyCoprodIso, a universe specialization of Stacks.AlgebraicGeometry.TopDegreeBaseChange .preservesColimitsOfShape_discrete_rightDerived_moduleGlobalSections, which is [Stacks, Tag 01FF] for a scheme), and [Stacks, Tag 089W] along the affine π identifies H^p(X, ∐ₙ Fₙ) with H^p(X', F') (Stacks.Cohomology.AffineComparison.cohomologyIsoPushforward). The B-action on ⨁ₙ H^p(X, Fₙ) is the one carried across that composite; it is not asserted to agree with the action the source defines degreewise from the graded module structure. That degreewise action over the f^* B̃ here is Stacks.AlgebraicGeometry.GradedProperCohomology.gradedTildeCohomologyGmodule, which is not restricted to the Rees algebra ⨁ₙ ℐⁿ of an ideal sheaf. The note on gradedCohomologySumModuleOfFiniteType records what the comparison of the two still needs, and moduleFinite_gradedTildeCohomologyModule is the finiteness it would yield. F' is chosen, so the action depends on that choice.

How F' and e are produced. The quasi-coherent half is already available: Stacks.AffineGradedAlgebra.exists_isQuasicoherent_pushforward_baseChange_iso_intCoprod produces a quasi-coherent 𝒪_{X'}-module whose direct image along π is ∐ₙ Fₙ, from hqc and nothing else — not even properness of f. It is the module of [Stacks, Tag 01SB] over Spec_X(𝓑) (Stacks.RelativeSpec.exists_iso_relativeSpecQcohPushforward_gradedModuleSheafOfRight_of_piece), read as an 𝒪_X-module through Stacks.AffineAlgebraEquivalence.restrictScalars_relativeSpecQcohEquivalence_functor_obj and Stacks.RelativeSpec.intCoprodIsoUnderlyingModule_gradedModuleSheaf, then transported to X' along Stacks.AffineGradedAlgebra.baseChangeIsoRelativeSpecGradedTildePullback, which is [Stacks, Tag 01LX] at 𝓑 = f^* B̃.

What that statement cannot give is coherence, because it forgets the 𝓑-action: the isomorphism it returns is one of 𝒪_X-modules and carries only the Γ(X, U)-action, while finite type of F' is taken over Γ(𝒪_{X'}, π⁻¹U). So the coherent F' is produced together with the identification in the quasi-coherent 𝓑-modules, by Stacks.AffineGradedAlgebra.exists_isFiniteType_pushforward_baseChange_iso_intCoprod, whose three transports — the span statement hidden in Stacks.Coherent.IsFiniteTypeOnAffine, the ring of sections of 𝓑 over an affine open, and the linearity of the identification over it — are the subject of StacksFrontier.AlgebraicGeometry.GradedProperCohomology.GradedModuleFiniteType. The upgrade from finite type to coherence is then (2) ⇒ (1) of [Stacks, Tag 01XZ], Stacks.AlgebraicGeometry.CoherentKernel.isCoherent_of_isQuasicoherent_isFiniteType, over the locally Noetherian X' of isLocallyNoetherian_baseChangeScheme.

The finiteness itself: B is Noetherian because it is a finitely generated algebra over the Noetherian ring A, and F' is coherent, so tag02O6 — [Stacks, Tag 02O6] over a ring — makes H^p(X', F') a finite B-module, and the comparison carries that finiteness back to ⨁ₙ H^p(X, Fₙ).

theorem moduleFinite_gradedCohomologySum_gradedPullback
    (A : Type u) [CommRing A] [IsNoetherianRing A] {B : Type u} [CommRing B] [Algebra A B]
    (𝒜 : ℕ → Submodule A B) [_root_.GradedAlgebra 𝒜] [Algebra.FiniteType A B]
    (f : X ⟶ Spec (.of A)) [IsProper f]
    (F : _root_.SheafOfModules.GradedModule
      (Stacks.Conormal.gradedPullback f (Stacks.AffineGradedAlgebra.gradedTildeOf A 𝒜)))
    (hqc : ∀ n : ℤ, (pieceModule F n).IsQuasicoherent)
    (hft : Stacks.Coherent.IsFiniteTypeOnAffine F) (p : ℕ) :
    @Module.Finite B (gradedCohomologySum F p) _ _
      (gradedCohomologySumModuleOfFiniteType A 𝒜 f F hqc hft p)

Sources

• Section 30.19, Tag 02O3
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.ProperCoherenceWitness.higherDirectImageIsCoherent · AlgebraicGeometry.ProperCoherenceWitness.isCoherent_pushforward · AlgebraicGeometry.ProperCoherenceWitness.moduleFinite_cohomology · Stacks.AlgebraicGeometry.GradedProperCohomology.exists_isZero_pieceTwistCohomology · Stacks.AlgebraicGeometry.GradedProperCohomology.moduleFinite_gradedCohomologySum_and_exists_isZero_pieceTwistCohomology · Stacks.AlgebraicGeometry.GradedProperCohomology.moduleFinite_gradedCohomologySum · Stacks.AlgebraicGeometry.GradedProperCohomology.moduleFinite_gradedCohomologySum_gradedPullback

Section30.20 The theorem on formal functions#

Section 30.20 of the Stacks Project, Tag 02O7. 10 tags here are carried by 20 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02O7, the section

Tag 02O7 in the Stacks Project.

Stacks.Blowup.pushforwardReesGradedModule, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/Completion/Quasicoherent/PushforwardIdealPowerGradedModule.lean, line 116. The attribute's comment: “⨁ₙ f_*(ℐⁿℱ) is a graded ⨁ₙ ℐⁿ-module on the base”.

[Stacks, Tag 02O7]: the graded ⨁ₙ ℐⁿ-module ⨁ₙ f_*(ℐⁿℱ) on the base, in degree zero. The maps pushforwardReesSmul make the pushforwards of the ideal-power multiples of ℱ a graded module over the Rees algebra of ℐ on Y.

Since f_* is left exact it is R ⁰ f_*, so this is the structure the source puts on ⨁ₙ R ᵖ f_*(ℐⁿℱ) for p = 0. Each axiom is the corresponding axiom of Stacks.Blowup.reesGradedModule on X, transported along the multiplicativity and unitality of Stacks.Blowup.reesPieceComap; the compatibility with restriction on Y is inherited from reesPieceComap being a morphism of sheaves.

public def pushforwardReesGradedModule : SheafOfModules.GradedModule (reesGradedAlgebra I)

Stacks.Blowup.pushforwardReesGradedModulePlus, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/Completion/Quasicoherent/PushforwardIdealPowerGradedModulePlus.lean, line 450. The attribute's comment: “⨁ₙ R ᵖ f_*(ℐⁿℱ) is a graded ⨁ₙ ℐⁿ-module on the base, in every degree p”. References: EGA III (3.3.1), “special case”.

[Stacks, Tag 02O7]: the graded ⨁ₙ ℐⁿ-module ⨁ₙ R ᵖ f_*(ℐⁿℱ) on the base, in every degree p. This is the structure the setup paragraph of the source obtains "by localizing and then sheafifying": the maps ℐⁱ ⊗_{𝒪_Y} R ᵖ f_*(ℐⁿℱ) ⟶ R ᵖ f_*(ℐⁿ⁺ⁱℱ), presented as the biadditive maps on sections that SheafOfModules.GradedModule consumes, together with the four laws.

Stacks.Blowup.pushforwardReesGradedModule is the same statement for p = 0, and is not superseded by this one: there the action is the multiplication of the Rees algebra on sections, by rfl, whereas here it divides by the higher direct image of the unit of AlgebraicGeometry.Scheme.Modules.restrictAdjunction, and the two agree at p = 0 only through R ⁰ f_* ≅ f_*.

public def pushforwardReesGradedModulePlus (f : X ⟶ Y) (I : Y.IdealSheafData) (F : X.Modules)
    (p : ℕ) : SheafOfModules.GradedModule (reesGradedAlgebra I)

Tag 02O8, a lemma

Tag 02O8 in the Stacks Project.

Stacks.Cohomology.FormalFunctions.isCohomologyReesFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalFunctions/ReesCohomologyFiniteReduction.lean, line 46. References: EGA III (3.3.2); EGA III (4.1.7.12), “more general”.

[Stacks, Tag 02O8]. For A Noetherian, f : X ⟶ Spec A proper and ℱ coherent, the graded module ⨁_{n ≥ 0} Hᵖ(X, Iⁿℱ) is a finite module over the Rees algebra B = ⨁_{n ≥ 0} Iⁿ.

This is Stacks.Cohomology.FormalFunctions.isCohomologyReesFinite_of_isCoherent, the reduction of the tag to [Stacks, Tag 0897] part (1) at a graded ⨁ₙ ℐⁿ-module, with that hypothesis supplied by Stacks.Cohomology.FormalFunctions.isCohomologyReesFiniteOfGradedModule.

public theorem isCohomologyReesFinite [IsNoetherianRing A]
    (F : X.left.Modules) [F.IsCoherent] (p : ℕ)
    (hX : AlgebraicGeometry.IsProper X.hom) :
    IsCohomologyReesFinite I X F p

Tag 02O9, a lemma

Tag 02O9 in the Stacks Project.

Stacks.Algebraization.isQuasicoherent_and_isFiniteType_pushforwardReesGradedModulePlus, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/Completion/Quasicoherent/HigherDirectImageFiniteTypeSpan.lean, line 426. References: EGA III (2.4.2), “special case”; SGA 2 XII (5.8), “(ii), special case”.

Stacks Project, Tag 02O9. Let f : X ⟶ Y be a morphism of schemes, ℱ an 𝒪_X-module and ℐ ⊆ 𝒪_Y a quasi-coherent sheaf of ideals, and assume Y locally Noetherian, f proper and ℱ coherent. Then the graded 𝒜 = ⨁ₙ ℐⁿ-module ℳ = ⨁ₙ R ᵖ f_*(ℐⁿℱ) = Stacks.Blowup.pushforwardReesGradedModulePlus f ℐ ℱ p is quasi-coherent — every homogeneous piece is — and of finite type over 𝒜.

This is the source's own argument. Quasi-coherence of a piece is [Stacks, Tag 01XJ] applied to ℐⁿℱ. Finite type is local on Y, and over an affine open V it is [Stacks, Tag 02O8] on the chart f⁻¹(V) ⟶ Spec Γ(Y, V), turned into the spanning family the affine criterion SheafOfModules.GradedModule.isFiniteType_of_affine_span consumes by Stacks.Algebraization.exists_affine_span_pushforwardReesGradedModulePlus.

Quasi-compactness and quasi-separatedness of f and quasi-coherence of ℱ are consequences of the source's hypotheses and are derived, not assumed.

public theorem isQuasicoherent_and_isFiniteType_pushforwardReesGradedModulePlus
    [IsLocallyNoetherian Y] [IsProper f] [F.IsCoherent] :
    (∀ n : ℤ, ((Stacks.Blowup.pushforwardReesGradedModulePlus f I F p).piece n).IsQuasicoherent) ∧
      (Stacks.Blowup.pushforwardReesGradedModulePlus f I F p).IsFiniteType
        (J := Opens.grothendieckTopology Y)

Tag 02OA, a lemma

Tag 02OA in the Stacks Project.

Stacks.Cohomology.FormalFunctions.exists_uniform_bound_cohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalFunctions/CohomologyIdealPowerSystem.lean, line 447. The attribute's comment: “parts (2) at n = 0 and (3); parts (1), (4), (5) and part (2) for n > 0 are not proved here”.

[Stacks, Tag 02OA], part (2) in the case n = 0 and part (3).

For A Noetherian, f : X → Spec A proper and ℱ coherent there is one integer c ≥ 0 such that

• the image of Hᵖ(X, Iʳℱ) → Hᵖ(X, ℱ) is contained in Iʳ⁻ᶜHᵖ(X, ℱ) for r ≥ c -- this is part (2) of the source at n = 0, where its e = max(0, c - n) is c; and
• Ker(Hᵖ(X, Iᵏℱ) → Hᵖ(X, ℱ)) = Ker(Hᵖ(X, Iᵏℱ) → Hᵖ(X, Iᵐℱ)) whenever m + c ≤ k -- this is part (3) of the source, which is the case m = k - c.

Parts (1), (4) and (5) of the source, and part (2) for general n, are not proved here; neither is the case n > 0 of part (2), which needs a compatibility between the transition maps and the multiplication maps that Stacks.RingTheory.IdealPowerSystem deliberately does not assume.

The hypothesis h02O8 is [Stacks, Tag 02O8] -- a different Stacks tag, absent from this branch -- carried in general form: it is quantified over every Noetherian base ring, every ideal of it, every proper scheme over it, every coherent module and every degree, and is instantiated inside the proof at the data of this statement. See IsCohomologyReesFinite for why it is absent and what is new about its being statable.

theorem exists_uniform_bound_cohomology [IsNoetherianRing A]
    (hX : AlgebraicGeometry.IsProper X.hom) (hF : SheafOfModules.IsCoherent F) (p : ℕ)
    (h02O8 : ∀ (A' : Type u) [CommRing A'] [IsNoetherianRing A'] (I' : Ideal A')
      (X' : Over (Spec (.of A'))) (_ : AlgebraicGeometry.IsProper X'.hom)
      (F' : X'.left.Modules) (_ : SheafOfModules.IsCoherent F') (p' : ℕ),
      (cohomologyIdealPowerSystem I' X' F' p').IsReesFinite) :
    ∃ c : ℕ,
      (∀ r : ℕ, c ≤ r → LinearMap.range (cohomologyProj I X F p r) ≤
        I ^ (r - c) • (⊤ : Submodule A (cohomology X F p))) ∧
      (∀ (m k : ℕ) (hmk : m + c ≤ k),
        LinearMap.ker (cohomologyProj I X F p k) =
          LinearMap.ker (cohomologyTr I X F p
            (show m ≤ k from le_trans (Nat.le_add_right m c) hmk)))

Stacks.Cohomology.FormalFunctions.exists_uniform_bound_cohomology_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionProper/ArtinReesChain.lean, line 104.

[Stacks, Tag 02OA]. For A Noetherian, I ⊆ A an ideal, f : X ⟶ Spec A proper and ℱ coherent there is one integer c ≥ 0 such that

1. the multiplication map Iʳ⁻ᶜ ⊗ Hᵖ(X, Iᶜℱ) → Hᵖ(X, Iʳℱ) is surjective for r ≥ c;
2. the image of Hᵖ(X, Iⁿ⁺ᵐℱ) → Hᵖ(X, Iⁿℱ) is contained in Iᵐ⁻ᵉHᵖ(X, Iⁿℱ) with e = max(0, c - n), whenever n + m ≥ c — and, in the shape where the target is Hᵖ(X, ℱ) itself rather than Hᵖ(X, I⁰ℱ), the image of Hᵖ(X, Iʳℱ) → Hᵖ(X, ℱ) is contained in Iʳ⁻ᶜHᵖ(X, ℱ) for r ≥ c, which is the source's n = 0;
3. Ker(Hᵖ(X, Iᵏℱ) → Hᵖ(X, ℱ)) = Ker(Hᵖ(X, Iᵏℱ) → Hᵖ(X, Iᵐℱ)) whenever m + c ≤ k, which is the source's part (3) in the case m = k - c;
4. there are A-linear maps cmp : IⁿHᵖ(X, ℱ) → Hᵖ(X, Iⁿ⁻ᶜℱ) for n ≥ c whose two composites with the canonical maps are canonical: cmp followed by Hᵖ(X, Iⁿ⁻ᶜℱ) → Hᵖ(X, ℱ) is the inclusion of IⁿHᵖ(X, ℱ) — which, read inside Iⁿ⁻²ᶜHᵖ(X, ℱ), where the image of Hᵖ(X, Iⁿ⁻ᶜℱ) → Hᵖ(X, ℱ) lies by part (2), is the source's composite IⁿHᵖ(X, ℱ) → Hᵖ(X, Iⁿ⁻ᶜℱ) → Iⁿ⁻²ᶜHᵖ(X, ℱ) — and, for n ≥ 2c, the image under cmp of the class of x ∈ Hᵖ(X, Iⁿℱ) in Iⁿ⁻ᶜHᵖ(X, ℱ) (the hypothesis (y : Hᵖ(X, ℱ)) = ... below says that y is that class, which lies in Iⁿ⁻ᶜHᵖ(X, ℱ) by part (2)) is the canonical image of x in Hᵖ(X, Iⁿ⁻²ᶜℱ);
5. the two inverse systems (Hᵖ(X, Iⁿℱ)) and (IⁿHᵖ(X, ℱ)) are pro-isomorphic, in the explicit up-to-refinement sense InverseSequence.ProIso.

Parts (1), (2) and (3) are the Artin-Rees argument for Rees systems, Stacks.RingTheory.ReesSystem.exists_uniform_bound_rees, run on Stacks.Cohomology.FormalFunctions.cohomologyIdealPowerSystem: its finiteness input is [Stacks, Tag 02O8], Stacks.Cohomology.FormalFunctions.isCohomologyReesFinite, and its two compatibility laws are cohomologyIdealPowerSystem_isTrMulCompatible. Parts (4) and (5) are Stacks.Cohomology.FormalFunctions.exists_comparison_cohomology, whose hypotheses are those three parts.

theorem exists_uniform_bound_cohomology_of_isProper [IsNoetherianRing A]
    (hX : AlgebraicGeometry.IsProper X.hom) [F.IsCoherent] (p : ℕ) :
    ∃ c : ℕ,
      (∀ r : ℕ, c ≤ r → Function.Surjective
        ((cohomologyTr I X F p (show r ≤ r - c + c by omega)).comp
          (cohomologyMulTensor I X F p (r - c) c))) ∧
      (∀ n m : ℕ, c ≤ n + m →
        LinearMap.range (cohomologyTr I X F p (Nat.le_add_right n m)) ≤
          I ^ (m - (c - n)) • (⊤ : Submodule A (cohomologyIdealPower I X F p n))) ∧
      (∀ r : ℕ, c ≤ r → LinearMap.range (cohomologyProj I X F p r) ≤
        I ^ (r - c) • (⊤ : Submodule A (cohomology X F p))) ∧
      (∀ (m k : ℕ) (hmk : m + c ≤ k),
        LinearMap.ker (cohomologyProj I X F p k) =
          LinearMap.ker (cohomologyTr I X F p
            (show m ≤ k from le_trans (Nat.le_add_right m c) hmk))) ∧
      (∃ cmp : ∀ n : ℕ, c ≤ n →
          ↥(I ^ n • (⊤ : Submodule A (cohomology X F p))) →ₗ[A]
            cohomologyIdealPower I X F p (n - c),
        (∀ (n : ℕ) (hn : c ≤ n) (y : ↥(I ^ n • (⊤ : Submodule A (cohomology X F p)))),
            cohomologyProj I X F p (n - c) (cmp n hn y) = (y : cohomology X F p)) ∧
          ∀ (n : ℕ) (hn : c + c ≤ n) (x : cohomologyIdealPower I X F p n)
            (y : ↥(I ^ (n - c) • (⊤ : Submodule A (cohomology X F p)))),
            (y : cohomology X F p) = cohomologyProj I X F p n x →
            cmp (n - c) (Nat.le_sub_of_add_le hn) y =
              cohomologyTr I X F p ((Nat.sub_le (n - c) c).trans (Nat.sub_le n c)) x) ∧
      Nonempty (InverseSequence.ProIso (cohomologyIdealPowerFunctor I X F p)
        (Stacks.RingTheory.idealPowerSmulSystem I (cohomology X F p)))

Tag 02OB, a lemma

Tag 02OB in the Stacks Project.

Stacks.Cohomology.FormalFunctions.exists_uniform_bound_cohomology_idealPowerQuotient_of_02O8, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalFunctions/FormalFunctionsFrom02O8.lean, line 192. The attribute's comment: “granted Tag 02O8, carried as the hypothesis h02O8”.

Stacks Project, Tag 02OB, granted [Stacks, Tag 02O8].

This is Stacks.Cohomology.FormalFunctions.exists_uniform_bound_cohomology_idealPowerQuotient with its two hypotheses discharged by Stacks.Cohomology.FormalFunctions.exists_uniform_bound_cohomology, applied in each degree q and transported along the identifications described in the implementation notes of this file. Nothing of the mathematics is new: the content is that the affine side of the theorem on formal functions rests on [Stacks, Tag 02O8] alone, which is carried here as the hypothesis h02O8 in the same general form exists_uniform_bound_cohomology consumes it.

public theorem exists_uniform_bound_cohomology_idealPowerQuotient_of_02O8
    (A : Type u) [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} (f : X ⟶ Spec (.of A))
    (hX : AlgebraicGeometry.IsProper f) (I : Ideal A) (F : X.Modules)
    (hF : SheafOfModules.IsCoherent F) (p : ℕ)
    (h02O8 : ∀ (A' : Type u) [CommRing A'] [IsNoetherianRing A'] (I' : Ideal A')
      (X' : Over (Spec (.of A'))) (_ : AlgebraicGeometry.IsProper X'.hom)
      (F' : X'.left.Modules) (_ : SheafOfModules.IsCoherent F') (p' : ℕ),
      (cohomologyIdealPowerSystem I' X' F' p').IsReesFinite) :
    ∃ c : ℕ,
      (∀ n : ℕ, c ≤ n →
          LinearMap.ker (cohomologyOverBaseMap A f p
              (cokernel.π (C := X.Modules)
                (idealPowerMultiple (baseIdealSheaf A I f) n F).ι)).hom ≤
            I ^ (n - c) • (⊤ : Submodule A (cohomologyOverBase A f p F))) ∧
        IsMittagLefflerCategorical
          (adicQuotientSystem (baseIdealSheaf A I f) F ⋙
            (moduleGlobalSections X).rightDerived p) ∧
        ∀ n k : ℕ, (hk : n + c ≤ k) →
          LinearMap.range (((moduleGlobalSections X).rightDerived p).map
              (idealPowerQuotientDrop (baseIdealSheaf A I f)
                ((Nat.le_add_right n c).trans hk) F)).hom =
            LinearMap.range (((moduleGlobalSections X).rightDerived p).map
              (cokernel.π (C := X.Modules)
                (idealPowerMultiple (baseIdealSheaf A I f) n F).ι)).hom

Stacks.Cohomology.FormalFunctions.exists_uniform_bound_cohomology_idealPowerQuotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalFunctions/IdealPowerQuotientCohomologyBound.lean, line 152. The attribute's comment: “granted Tag 02OA, carried as the hypotheses h02OA_image and h02OA_kernel”.

Stacks Project, Tag 02OB, granted [Stacks, Tag 02OA].

There is a single c ≥ 0 such that, with 𝓘 = I · 𝒪_X:

1. Ker(H^p(X, ℱ) → H^p(X, ℱ / 𝓘 ^ n ℱ)) ⊆ I ^ (n - c) · H^p(X, ℱ) for every n ≥ c;
2. the inverse system n ↦ H^p(X, ℱ / 𝓘 ^ n ℱ) satisfies the Mittag-Leffler condition;
3. for every k ≥ n + c, the image of H^p(X, ℱ / 𝓘 ^ k ℱ) in H^p(X, ℱ / 𝓘 ^ n ℱ) equals the image of H^p(X, ℱ).

The two hypotheses are the clauses of [Stacks, Tag 02OA] that the source's proof uses, each quantified over the degree because the proof applies them in degrees p and p + 1 and takes the larger of the two constants: h02OA_image is clause (2) of that lemma in the case n = 0, and h02OA_kernel is its clause (3). The source's standing hypotheses — A Noetherian, f proper and ℱ coherent — are what make [Stacks, Tag 02OA] true and are used nowhere else, so they do not appear.

Clause (1) is the kernel-image identity of the long exact sequence of 0 → 𝓘 ^ n ℱ → ℱ → ℱ / 𝓘 ^ n ℱ → 0 followed by h02OA_image. Clause (3) is the diagram chase along the ladder of those sequences: naturality of the connecting map carries a class of H^p(X, ℱ / 𝓘 ^ k ℱ) to one annihilated by the connecting map of the exponent-n sequence, because h02OA_kernel in degree p + 1 identifies the kernel of H^(p+1)(𝓘 ^ k ℱ) → H^(p+1)(ℱ) with a kernel that H^(p+1)(𝓘 ^ k ℱ) → H^(p+1)(𝓘 ^ n ℱ) factors through. Clause (2) follows from clause (3).

public theorem exists_uniform_bound_cohomology_idealPowerQuotient
    (h02OA_image : ∀ q : ℕ, ∃ c : ℕ, ∀ k : ℕ, c ≤ k →
      LinearMap.range (cohomologyOverBaseMap A f q
          (idealPowerMultiple (baseIdealSheaf A I f) k F).ι).hom ≤
        I ^ (k - c) • (⊤ : Submodule A (cohomologyOverBase A f q F)))
    (h02OA_kernel : ∀ q : ℕ, ∃ c : ℕ, ∀ k : ℕ, c ≤ k →
      LinearMap.ker (((moduleGlobalSections X).rightDerived q).map
          (idealPowerMultiple (baseIdealSheaf A I f) k F).ι).hom =
        LinearMap.ker (((moduleGlobalSections X).rightDerived q).map
          (submoduleInclusion (idealPowerMultiple_antitone (baseIdealSheaf A I f) F
            (Nat.sub_le k c)))).hom) :
    ∃ c : ℕ,
      (∀ n : ℕ, c ≤ n →
          LinearMap.ker (cohomologyOverBaseMap A f p
              (cokernel.π (C := X.Modules)
                (idealPowerMultiple (baseIdealSheaf A I f) n F).ι)).hom ≤
            I ^ (n - c) • (⊤ : Submodule A (cohomologyOverBase A f p F))) ∧
        IsMittagLefflerCategorical
          (adicQuotientSystem (baseIdealSheaf A I f) F ⋙
            (moduleGlobalSections X).rightDerived p) ∧
        ∀ n k : ℕ, (hk : n + c ≤ k) →
          LinearMap.range (((moduleGlobalSections X).rightDerived p).map
              (idealPowerQuotientDrop (baseIdealSheaf A I f)
                ((Nat.le_add_right n c).trans hk) F)).hom =
            LinearMap.range (((moduleGlobalSections X).rightDerived p).map
              (cokernel.π (C := X.Modules)
                (idealPowerMultiple (baseIdealSheaf A I f) n F).ι)).hom

Stacks.Cohomology.FormalFunctions.exists_uniform_bound_cohomology_idealPowerQuotient_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionProper/ArtinReesChain.lean, line 180. References: SGA 2 IX (1.1), “Clause (3), special case”; SGA 2 IX (2.1), “(iii)”.

[Stacks, Tag 02OB]. For A Noetherian, J ⊆ A an ideal, f : X ⟶ Spec A proper and ℱ coherent there is a single c ≥ 0 such that, with 𝓙 = J · 𝒪_X:

1. Ker(Hᵖ(X, ℱ) → Hᵖ(X, ℱ / 𝓙ⁿℱ)) ⊆ Jⁿ⁻ᶜHᵖ(X, ℱ) for every n ≥ c;
2. the inverse system n ↦ Hᵖ(X, ℱ / 𝓙ⁿℱ) satisfies the Mittag-Leffler condition;
3. for every k ≥ n + c the image of Hᵖ(X, ℱ / 𝓙ᵏℱ) in Hᵖ(X, ℱ / 𝓙ⁿℱ) equals the image of Hᵖ(X, ℱ).

This is Stacks.Cohomology.FormalFunctions.exists_uniform_bound_cohomology_idealPowerQuotient_of_02O8 with its hypothesis, [Stacks, Tag 02O8] in general form, discharged by Stacks.FormalFunctions.isReesFinite_cohomologyIdealPowerSystem.

theorem exists_uniform_bound_cohomology_idealPowerQuotient_of_isProper [IsNoetherianRing A]
    (hf : AlgebraicGeometry.IsProper f) [G.IsCoherent] (p : ℕ) :
    ∃ c : ℕ,
      (∀ n : ℕ, c ≤ n →
          LinearMap.ker (cohomologyOverBaseMap A f p
              (cokernel.π (C := X.Modules)
                (idealPowerMultiple (baseIdealSheaf A J f) n G).ι)).hom ≤
            J ^ (n - c) • (⊤ : Submodule A (cohomologyOverBase A f p G))) ∧
        IsMittagLefflerCategorical
          (adicQuotientSystem (baseIdealSheaf A J f) G ⋙
            (Stacks.Cohomology.AffineBase.moduleGlobalSections X).rightDerived p) ∧
        ∀ n k : ℕ, (hk : n + c ≤ k) →
          LinearMap.range
              (((Stacks.Cohomology.AffineBase.moduleGlobalSections X).rightDerived p).map
                (idealPowerQuotientDrop (baseIdealSheaf A J f)
                  ((Nat.le_add_right n c).trans hk) G)).hom =
            LinearMap.range
              (((Stacks.Cohomology.AffineBase.moduleGlobalSections X).rightDerived p).map
                (cokernel.π (C := X.Modules)
                  (idealPowerMultiple (baseIdealSheaf A J f) n G).ι)).hom

Tag 02OC, a theorem

Tag 02OC in the Stacks Project.

Stacks.Cohomology.FormalFunctions.formalFunctionsEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalFunctions/AdicCompletionLimitComparison.lean, line 264. The attribute's comment: “the isomorphism of A-modules only, not the homeomorphism for the limit topologies; granted Tag 02OB, whose clauses (1) and (3) are carried as the hypotheses h02OB_ker and h02OB_range”.

Stacks Project, Tag 02OC, granted [Stacks, Tag 02OB], and for the A-module isomorphism only.

With 𝓘 = I · 𝒪_X, the I-adic completion of H^p(X, ℱ) is the limit of the tower n ↦ H^p(X, ℱ / 𝓘 ^ n ℱ). The map is the one assembled from the projections H^p(X, ℱ) ⟶ H^p(X, ℱ / 𝓘 ^ n ℱ), which is the content of formalFunctionsEquiv_proj_of. [Stacks, Tag 02OC] further asserts that the comparison is a homeomorphism for the limit topologies; that is not proved here, and no statement in this file claims it.

The two hypotheses are clauses (1) and (3) of [Stacks, Tag 02OB], for a fixed c, in the shape Stacks.Cohomology.FormalFunctions.exists_uniform_bound_cohomology_idealPowerQuotient produces them: h02OB_ker bounds the kernel of the n-th projection by I ^ (n - c) H^p(X, ℱ), and h02OB_range says that for k ≥ n + c the image of H^p(X, ℱ / 𝓘 ^ k ℱ) in H^p(X, ℱ / 𝓘 ^ n ℱ) is the image of H^p(X, ℱ). Clause (2) of that lemma, the Mittag-Leffler condition, is not needed: in this formulation it is subsumed by clause (3). The source's standing hypotheses — A Noetherian, f proper and ℱ coherent — are what make [Stacks, Tag 02OB] true and are used nowhere else, so only quasi-coherence of ℱ, which the annihilation argument needs, appears.

Everything else is Stacks.IntertwinedFiltration.adicCompletionEquivTowerLimit, the source's own argument carried out abstractly.

public def formalFunctionsEquiv [F.IsQuasicoherent]
    (h02OB_ker : ∀ n : ℕ, c ≤ n →
      LinearMap.ker (adicCohomologyProj A f I F p n) ≤
        I ^ (n - c) • (⊤ : Submodule A (cohomologyOverBase A f p F)))
    (h02OB_range : ∀ n k : ℕ, (hk : n + c ≤ k) →
      LinearMap.range (((moduleGlobalSections X).rightDerived p).map
          (idealPowerQuotientDrop (baseIdealSheaf A I f)
            ((Nat.le_add_right n c).trans hk) F)).hom =
        LinearMap.range (((moduleGlobalSections X).rightDerived p).map
          (cokernel.π (C := X.Modules)
            (idealPowerMultiple (baseIdealSheaf A I f) n F).ι)).hom) :
    AdicCompletion I (cohomologyOverBase A f p F) ≃ₗ[A]
      towerLimit (adicCohomologyTower A f I F p) (adicCohomologyTowerMap A f I F p)

Stacks.Cohomology.FormalFunctions.formalFunctionsEquiv_proj_of, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalFunctions/AdicCompletionLimitComparison.lean, line 292. The attribute's comment: “the identification of the isomorphism of formalFunctionsEquiv as the one assembled from the projections; same hypotheses, and again nothing about the limit topologies”.

The comparison isomorphism of [Stacks, Tag 02OC] is the canonical one: its n-th component carries the image in H^p(X, ℱ) ^∧_I of a class x ∈ H^p(X, ℱ) to the image of x in H^p(X, ℱ / 𝓘 ^ n ℱ). Together with formalFunctionsEquiv this says that the maps H^p(X, ℱ) / I ^ n H^p(X, ℱ) ⟶ H^p(X, ℱ / 𝓘 ^ n ℱ) assemble into an isomorphism, rather than merely that the two modules are isomorphic.

public lemma formalFunctionsEquiv_proj_of [F.IsQuasicoherent]
    (h02OB_ker : ∀ n : ℕ, c ≤ n →
      LinearMap.ker (adicCohomologyProj A f I F p n) ≤
        I ^ (n - c) • (⊤ : Submodule A (cohomologyOverBase A f p F)))
    (h02OB_range : ∀ n k : ℕ, (hk : n + c ≤ k) →
      LinearMap.range (((moduleGlobalSections X).rightDerived p).map
          (idealPowerQuotientDrop (baseIdealSheaf A I f)
            ((Nat.le_add_right n c).trans hk) F)).hom =
        LinearMap.range (((moduleGlobalSections X).rightDerived p).map
          (cokernel.π (C := X.Modules)
            (idealPowerMultiple (baseIdealSheaf A I f) n F).ι)).hom)
    (n : ℕ) (x : cohomologyOverBase A f p F) :
    towerLimit.proj n (formalFunctionsEquiv A f I F p c h02OB_ker h02OB_range
        (AdicCompletion.of I (cohomologyOverBase A f p F) x)) =
      adicCohomologyProj A f I F p n x

Stacks.Cohomology.FormalFunctions.exists_formalFunctionsEquiv_of_02O8, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalFunctions/FormalFunctionsFrom02O8.lean, line 238. The attribute's comment: “granted Tag 02O8, carried as the hypothesis h02O8”.

Stacks Project, Tag 02OC, granted [Stacks, Tag 02O8], and for the A-module isomorphism only.

With 𝓘 = I · 𝒪_X, the I-adic completion of Hᵖ(X, ℱ) is the limit of the tower n ↦ Hᵖ(X, ℱ / 𝓘ⁿℱ), by the comparison map: the projection normalisation says that the n-th component of the equivalence carries the image of a class x ∈ Hᵖ(X, ℱ) to the image of x in Hᵖ(X, ℱ / 𝓘ⁿℱ). The constant c is existentially bound because Stacks.Cohomology.FormalFunctions.formalFunctionsEquiv is indexed by it.

[Stacks, Tag 02OC] further asserts that the comparison is a homeomorphism for the limit topologies; that is not proved here, exactly as in Stacks.Cohomology.FormalFunctions.formalFunctionsEquiv, and this statement does not claim it.

Quasi-coherence of ℱ is not assumed: it follows from hF.

public theorem exists_formalFunctionsEquiv_of_02O8
    (A : Type u) [CommRing A] [IsNoetherianRing A] {X : Scheme.{u}} (f : X ⟶ Spec (.of A))
    (hX : AlgebraicGeometry.IsProper f) (I : Ideal A) (F : X.Modules)
    (hF : SheafOfModules.IsCoherent F) (p : ℕ)
    (h02O8 : ∀ (A' : Type u) [CommRing A'] [IsNoetherianRing A'] (I' : Ideal A')
      (X' : Over (Spec (.of A'))) (_ : AlgebraicGeometry.IsProper X'.hom)
      (F' : X'.left.Modules) (_ : SheafOfModules.IsCoherent F') (p' : ℕ),
      (cohomologyIdealPowerSystem I' X' F' p').IsReesFinite) :
    ∃ (c : ℕ) (e : AdicCompletion I (cohomologyOverBase A f p F) ≃ₗ[A]
        towerLimit (adicCohomologyTower A f I F p) (adicCohomologyTowerMap A f I F p)),
      ∀ (n : ℕ) (x : cohomologyOverBase A f p F),
        towerLimit.proj n (e (AdicCompletion.of I (cohomologyOverBase A f p F) x)) =
          adicCohomologyProj A f I F p n x

Stacks.Cohomology.FormalFunctions.exists_formalFunctionsEquiv_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionProper/ArtinReesChain.lean, line 236. References: EGA III (4.1.7).

[Stacks, Tag 02OC]. For A Noetherian, I ⊆ A an ideal, f : X ⟶ Spec A proper and ℱ coherent, the maps Hᵖ(X, ℱ)/IⁿHᵖ(X, ℱ) → Hᵖ(X, ℱ/𝓘ⁿℱ) assemble into an isomorphism

Hᵖ(X, ℱ)^∧_I ≅ limₙ Hᵖ(X, ℱ/𝓘ⁿℱ)

of A-modules, and that isomorphism is a homeomorphism for the limit topologies.

The second component says that the n-th projection of the isomorphism carries the image of a class x ∈ Hᵖ(X, ℱ) to the image of x in Hᵖ(X, ℱ/𝓘ⁿℱ), so the isomorphism is the one the source's system of maps defines and not merely some isomorphism between the two modules. The third is the source's further assertion: the limit topology on Hᵖ(X, ℱ)^∧_I = limₙ Hᵖ(X, ℱ)/Iⁿ and the limit topology on limₙ Hᵖ(X, ℱ/𝓘ⁿℱ) correspond under it. By Stacks.IntertwinedFiltration.adicCompletionModuleLimitTopology_eq_adicModuleTopology the topology on the left is equally the I-adic topology of the completion, which is the source's own footnote to the statement.

The module isomorphism is Stacks.Cohomology.FormalFunctions.formalFunctionsEquiv together with formalFunctionsEquiv_proj_of, and the homeomorphism is Stacks.IntertwinedFiltration.isHomeomorph_adicCompletionEquivTowerLimit_limitTopology for the same map; the hypotheses of all three are clauses (1) and (3) of [Stacks, Tag 02OB], which come from exists_uniform_bound_cohomology_idealPowerQuotient_of_isProper, together with the finite generation of I that IsNoetherianRing A supplies.

theorem exists_formalFunctionsEquiv_of_isProper [IsNoetherianRing A]
    (hf : AlgebraicGeometry.IsProper f) [F.IsCoherent] (p : ℕ) :
    ∃ e : AdicCompletion I (cohomologyOverBase A f p F) ≃ₗ[A]
        towerLimit (adicCohomologyTower A f I F p) (adicCohomologyTowerMap A f I F p),
      (∀ (n : ℕ) (x : cohomologyOverBase A f p F),
          towerLimit.proj n (e (AdicCompletion.of I (cohomologyOverBase A f p F) x)) =
            adicCohomologyProj A f I F p n x) ∧
        @IsHomeomorph _ _
          (adicCompletionModuleLimitTopology (M := cohomologyOverBase A f p F) I)
          (towerLimit.limitTopology (adicCohomologyTower A f I F p)
            (adicCohomologyTowerMap A f I F p)) e

Tag 087U, a lemma

Tag 087U in the Stacks Project.

Stacks.Algebraization.isIso_cohomologyToLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionProper/FormalFunctions.lean, line 360. The attribute's comment: “for all p ≥ 0 and any f : X ⟶ Spec A with X locally Noetherian, hence in particular for a proper f; the finiteness of the cohomology (02O6) and the two uniform Artin-Rees bounds (02OB) enter as the hypotheses hfin, hker and hstab, none of which this library carries for a proper morphism”.

Stacks 087U, granted the two uniform bounds of [Stacks, Tag 02OB] and the finiteness of [Stacks, Tag 02O6].

Let A be a Noetherian ring complete with respect to an ideal J, let X be a locally Noetherian scheme over A and let F be a coherent sheaf on X. Then for every p ≥ 0 the canonical map

Hᵖ(X, F) ⟶ limₙ Hᵖ(X, F / Jⁿ F)

is an isomorphism, provided

• hfin: Hᵖ(X, F) is a finite A-module — this is [Stacks, Tag 02O6], the finiteness of the cohomology of a coherent sheaf along a proper morphism, which is not available in this library for a proper morphism;
• hker: there is a c with ker (Hᵖ(X, F) ⟶ Hᵖ(X, F / Jⁿ⁺ᶜ F)) ⊆ Jⁿ Hᵖ(X, F) for all n;
• hstab: there is a c such that the image of Hᵖ(X, F) ⟶ Hᵖ(X, F / Jⁿ F) contains the image of Hᵖ(X, F / Jⁿ⁺ᶜ F) ⟶ Hᵖ(X, F / Jⁿ F) for all n.

The last two are the uniform Artin-Rees bounds of [Stacks, Tag 02OB], read through the long exact cohomology sequences of 0 → Jⁿ F → F → F / Jⁿ F → 0; they are the two places where properness of the structure morphism enters the source's argument, and neither is available in this library — see the implementation notes of StacksFrontier/RingTheory/LocalCohomology/UniformCohomologyBound.lean.

What is proved here is everything else: the completion step of the source's proof — that no completion is needed on the left because a finite module over a complete Noetherian ring is itself complete — together with the derivation of the comparison from the two bounds.

public theorem isIso_cohomologyToLimit (A : Type u) [CommRing A] [IsNoetherianRing A]
    (J : Ideal A) [IsAdicComplete J A] {X : Scheme.{u}} [IsLocallyNoetherian X]
    (f : X ⟶ Spec (.of A))
    (F : AlgebraicGeometry.SheafOfModules.CoherentModules X.ringCatSheaf) (p : ℕ)
    (hfin : letI := baseAlgebra A f
      Module.Finite A
        ↥(((Stacks.Cohomology.AffineBase.moduleGlobalSections X).rightDerived p).obj F.obj))
    (hker : letI := baseAlgebra A f
      ∃ c : ℕ, ∀ (n : ℕ) (x : ↥(((Stacks.Cohomology.AffineBase.moduleGlobalSections
          X).rightDerived p).obj F.obj)),
        (((Stacks.Cohomology.AffineBase.moduleGlobalSections X).rightDerived p).map
            (completionProjection X
              (Stacks.Cohomology.FormalFunctions.baseIdealSheaf A J f) F (n + c))).hom x = 0 →
          x ∈ J ^ n • (⊤ : Submodule A ↥(((Stacks.Cohomology.AffineBase.moduleGlobalSections
            X).rightDerived p).obj F.obj)))
    (hstab : ∃ c : ℕ, ∀ (n : ℕ)
        (y : ↥((completionCohomologySystem
          (Stacks.Cohomology.FormalFunctions.baseIdealSheaf A J f) F p).obj (op (n + c)))),
        ∃ x : ↥(((Stacks.Cohomology.AffineBase.moduleGlobalSections X).rightDerived p).obj F.obj),
          (((Stacks.Cohomology.AffineBase.moduleGlobalSections X).rightDerived p).map
              (completionProjection X
                (Stacks.Cohomology.FormalFunctions.baseIdealSheaf A J f) F n)).hom x =
            ((completionCohomologySystem
                (Stacks.Cohomology.FormalFunctions.baseIdealSheaf A J f) F p).map
              (homOfLE (Nat.le_add_right n c)).op).hom y) :
    IsIso (cohomologyToLimit
      (Stacks.Cohomology.FormalFunctions.baseIdealSheaf A J f) F p)

Stacks.Algebraization.isIso_cohomologyToLimit_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionProper/FormalFunctions.lean, line 464. The attribute's comment: “for a proper f and all p ≥ 0; the finiteness of the cohomology (02O6) and the two uniform Artin-Rees bounds (02OB) enter as the hypotheses hfin, hker and hstab, none of which this library carries for a proper morphism”.

Stacks 087U for a proper morphism, granted the two uniform bounds of [Stacks, Tag 02OB] and the finiteness of [Stacks, Tag 02O6].

This is Stacks.Algebraization.isIso_cohomologyToLimit with the hypothesis IsLocallyNoetherian X replaced by properness of f, which implies it over a Noetherian base. The statement is then the source's verbatim: A Noetherian and J-adically complete, f : X ⟶ Spec A proper, F coherent, and the conclusion for every p ≥ 0.

The three hypotheses are the ones the source cites and the only places properness is used there; none of them is carried by this library for a proper morphism. See Stacks.Algebraization.isIso_cohomologyToLimit for what each of them says.

public theorem isIso_cohomologyToLimit_of_isProper (A : Type u) [CommRing A] [IsNoetherianRing A]
    (J : Ideal A) [IsAdicComplete J A] {X : Scheme.{u}} (f : X ⟶ Spec (.of A)) [IsProper f]
    (F : AlgebraicGeometry.SheafOfModules.CoherentModules X.ringCatSheaf) (p : ℕ)
    (hfin : letI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian f
      letI := baseAlgebra A f
      Module.Finite A
        ↥(((Stacks.Cohomology.AffineBase.moduleGlobalSections X).rightDerived p).obj F.obj))
    (hker : letI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian f
      letI := baseAlgebra A f
      ∃ c : ℕ, ∀ (n : ℕ) (x : ↥(((Stacks.Cohomology.AffineBase.moduleGlobalSections
          X).rightDerived p).obj F.obj)),
        (((Stacks.Cohomology.AffineBase.moduleGlobalSections X).rightDerived p).map
            (completionProjection X
              (Stacks.Cohomology.FormalFunctions.baseIdealSheaf A J f) F (n + c))).hom x = 0 →
          x ∈ J ^ n • (⊤ : Submodule A ↥(((Stacks.Cohomology.AffineBase.moduleGlobalSections
            X).rightDerived p).obj F.obj)))
    (hstab : letI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian f
      ∃ c : ℕ, ∀ (n : ℕ)
        (y : ↥((completionCohomologySystem
          (Stacks.Cohomology.FormalFunctions.baseIdealSheaf A J f) F p).obj (op (n + c)))),
        ∃ x : ↥(((Stacks.Cohomology.AffineBase.moduleGlobalSections X).rightDerived p).obj F.obj),
          (((Stacks.Cohomology.AffineBase.moduleGlobalSections X).rightDerived p).map
              (completionProjection X
                (Stacks.Cohomology.FormalFunctions.baseIdealSheaf A J f) F n)).hom x =
            ((completionCohomologySystem
                (Stacks.Cohomology.FormalFunctions.baseIdealSheaf A J f) F p).map
              (homOfLE (Nat.le_add_right n c)).op).hom y) :
    letI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian f
    IsIso (cohomologyToLimit
      (Stacks.Cohomology.FormalFunctions.baseIdealSheaf A J f) F p)

Declarations registered for the tag:

• Stacks.Algebraization.isIso_cohomologyToLimit_of_isProper_of_isAdicComplete, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionProper/ArtinReesChain.lean, line 270 (StacksFrontier).

Tag 02OD, a lemma

Tag 02OD in the Stacks Project.

Stacks.FormalFunctions.nonempty_adicCompletionHigherDirectImageStalkEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalFunctions/CompletionStalkLimit.lean, line 119. References: EGA III (4.2.4), “Degree p = 0 case”.

Stacks Project, Tag 02OD. Let f : X ⟶ Y be a proper morphism of schemes with Y locally Noetherian, let ℱ be a coherent 𝒪_X-module and let y be a point of Y. Let X_n = Spec (𝒪_{Y, y}/𝔪_y ⁿ) ×_Y X be the infinitesimal neighbourhoods of the fibre X_y and ℱ_n = i_n ^* ℱ. Then in every degree p

(R ᵖ f_* ℱ) _y ^∧ ≅ lim_n H ᵖ (X_n, ℱ_n)

as 𝒪 ^∧_{Y, y}-modules.

public theorem nonempty_adicCompletionHigherDirectImageStalkEquiv (f : X ⟶ Y)
    [IsLocallyNoetherian Y] [IsProper f] (F : X.Modules) [F.IsCoherent] (y : Y) (p : ℕ) :
    Nonempty
      (AdicCompletion (stalkMaximalIdeal y) (higherDirectImageStalk f F y p) ≃ₗ[
          AdicCompletion (stalkMaximalIdeal y) (Y.presheaf.stalk y)]
        towerLimit (infinitesimalCohomology f F y p) (infinitesimalCohomologyMap f F y p))

Stacks.Cohomology.FormalFunctions.pushforwardPullbackBaseIdealIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalFunctions/FormalFunctionsTheorem/IdealPowerQuotientSubscheme.lean, line 175. The attribute's comment: “the second step of the tag's proof: the identification i_{n*} ℱ_n ≅ ℱ / 𝔪ⁿ ℱ, over an affine base and for the quotient by the n-th power of the ideal sheaf generated by an ideal of that base. The tag's conclusion is NOT asserted: that needs Tag 02OC, which rests on Tag 02O8, together with Tag 02KH”.

i_{n*} ℱ_n ≅ ℱ / I ⁿ ℱ. The direct image of the restriction of ℱ to the infinitesimal neighbourhood X_n = X ×_{Spec A} Spec (A / I ⁿ) is the quotient of ℱ by the n-th power of the ideal sheaf I · 𝒪_X.

This is the second step of the proof of [Stacks, Tag 02OD], not its conclusion: the source derives H ᵖ (X_n, ℱ_n) = H ᵖ (X, ℱ / 𝔪 ⁿ ℱ) from it by the Leray spectral sequence for i_n together with [Stacks, Tag 01Y6]. At p = 0 no spectral sequence is needed, because a direct image does not change global sections, so the global sections of this isomorphism are that identification. The tag's conclusion — that the completed stalk of R ᵖ f_* ℱ at y is the limit of the H ᵖ (X_n, ℱ_n) — is not asserted here: it needs in addition [Stacks, Tag 02OC], which rests on [Stacks, Tag 02O8], and flat base change [Stacks, Tag 02KH] to reduce Y to Spec 𝒪_{Y,y}, which is the reduction that makes i_n a closed immersion in the first place.

The underlying mathematics is [Stacks, Tag 0EL1], already proved in the library as Stacks.Algebraization.idealQuotientPushforwardIso; what is asserted here is that the fibre product of the source's diagram is a presentation it applies to.

public def pushforwardPullbackBaseIdealIso :
    (Scheme.Modules.pushforward (baseNeighbourhoodι A I f n)).obj
        ((Scheme.Modules.pullback (baseNeighbourhoodι A I f n)).obj F) ≅
      idealPowerQuotient (baseIdealSheaf A I f) n F

Stacks.FormalFunctions.infinitesimalNeighbourhood, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalFunctions/InfinitesimalNeighbourhood.lean, line 260. The attribute's comment: “the infinitesimal neighbourhoods X_n = X ×_Y Spec(𝒪_{Y,y}/𝔪ⁿ) of the fibre, the setup paragraph of the tag. The conclusion -- that the completed stalk of R^p f_* ℱ at y is the limit of the H^p(X_n, ℱ_n) -- is NOT asserted here: see the implementation notes for its three inputs and which of them are now available”.

The n-th infinitesimal neighbourhood X_n = Spec (𝒪_{Y,y}/𝔪_y ^ n) ×_Y X of the fibre of f : X ⟶ Y over y.

public abbrev infinitesimalNeighbourhood (f : X ⟶ Y) (y : Y) (n : ℕ) : Scheme.{u}

Tag 02OE, a lemma

Tag 02OE in the Stacks Project.

Stacks.FormalFunctions.isZero_stalk_higherDirectImage_of_finite_fibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalFunctions/FiniteFibreVanishing.lean, line 142.

Stacks Project, Tag 02OE. Let f : X ⟶ Y be a morphism of schemes and let y : Y. Assume Y is locally Noetherian, f is proper, and the fibre f ⁻¹' {y} is finite. Then for every coherent 𝒪_X-module F and every p > 0 the stalk (R ᵖ f_* F)_y vanishes.

This is isZero_stalk_higherDirectImage_of_finite_preimage, which needs neither hypothesis; coherence of F gives quasi-coherence through [Stacks, Tag 01BW] (Stacks.AlgebraicGeometry.CoherentTFAE.isQuasicoherent_isFiniteType_of_isCoherent), for which no hypothesis on Y is needed either. Both hypotheses are kept here because the tag states them.

theorem isZero_stalk_higherDirectImage_of_finite_fibre {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsLocallyNoetherian Y] [IsProper f] (y : Y) (hfin : (f ⁻¹' {y}).Finite) (F : X.Modules)
    [F.IsCoherent] (p : ℤ) (hp : 0 < p) :
    IsZero
      ((((Scheme.Modules.pushforward f).rightDerivedPlus p).obj F).presheaf.stalk y)

Tag 02V7, a lemma

Tag 02V7 in the Stacks Project.

Stacks.AlgebraicGeometry.FibreDimension.isZero_stalk_rightDerivedPlus_of_fiber_dimension_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/HigherDirectImageFibreDimension/GeneralDimension.lean, line 133. References: EGA III (4.2.2), “partial”; SGA 6 X (4.4), “Stalk form of (4.4.5)”.

[Stacks, Tag 02V7]. Let f : X ⟶ Y be a morphism of schemes and let y ∈ Y. Assume Y locally Noetherian, f proper and dim(X_y) = d. Then for every coherent sheaf ℱ on X we have (Rᵖ f_* ℱ)_y = 0 for all p > d.

The fibre dimension is taken as the upper bound dim(X_y) ≤ d, which is what the proof uses. A neighbourhood V of y over which every fibre is bounded by d is produced by AlgebraicGeometry.exists_isAffineOpen_forall_topologicalKrullDim_fiber_le; the stalk at y of the higher direct image along f is the one along f ∣_ V; over the affine base V the higher direct image vanishes as soon as the cohomology of f ⁻¹ V does; and that vanishing is isZero_rightDerived_moduleGlobalSections_of_affine_base.

theorem isZero_stalk_rightDerivedPlus_of_fiber_dimension_le
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsProper f] [IsLocallyNoetherian Y] (y : Y) (d : ℕ)
    (hdim : topologicalKrullDim (f.fiber y) ≤ (d : WithBot ℕ∞))
    (F : X.Modules) [F.IsCoherent] (p : ℤ) (hp : (d : ℤ) < p) :
    IsZero ((((Scheme.Modules.pushforward f).rightDerivedPlus p).obj F).presheaf.stalk y)

Sources

• Section 30.20, Tag 02O7
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Blowup.pushforwardReesGradedModule · Stacks.Blowup.pushforwardReesGradedModulePlus · Stacks.Cohomology.FormalFunctions.isCohomologyReesFinite · Stacks.Algebraization.isQuasicoherent_and_isFiniteType_pushforwardReesGradedModulePlus · Stacks.Cohomology.FormalFunctions.exists_uniform_bound_cohomology · Stacks.Cohomology.FormalFunctions.exists_uniform_bound_cohomology_of_isProper · Stacks.Cohomology.FormalFunctions.exists_uniform_bound_cohomology_idealPowerQuotient_of_02O8 · Stacks.Cohomology.FormalFunctions.exists_uniform_bound_cohomology_idealPowerQuotient

Section30.21 Applications of the theorem on formal functions#

Section 30.21 of the Stacks Project, Tag 02OF. 4 tags here are carried by 3 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02OG, a lemma

Tag 02OG in the Stacks Project.

Declarations registered for the tag:

• AlgebraicGeometry.IsFinite.tfae_isProper_finite_preimage_singleton, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/FormalFunctions/FiniteIffProperFiniteFibres.lean, line 32 (StacksFrontier): “the equivalence of the first two conditions, for an arbitrary target; the source assumes it locally Noetherian”.

Tag 02OH, a lemma

Tag 02OH in the Stacks Project.

Stacks.FormalFunctions.exists_isFinite_morphismRestrict_of_finite_fibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalFunctions/FiniteFibreVanishing.lean, line 161. References: EGA III (4.8.11), “ordinary schemes”.

Stacks Project, Tag 02OH. Let f : X ⟶ Y be a morphism of schemes and let y : Y. Assume Y is locally Noetherian, f is proper, and the fibre f ⁻¹' {y} is finite. Then y has an open neighbourhood V over which f is finite, that is, f ∣_ V : f ⁻¹ᵁ V ⟶ V is finite.

This is Zariski's main theorem in the form of [Stacks, Tag 02UP] (AlgebraicGeometry.exists_isFinite_morphismRestrict_of_finite_preimage_singleton), which needs no hypothesis on Y; local Noetherianness is kept here because the tag states it. The source instead deduces the lemma from Tag 02OG, finiteness being equivalent to properness with finite fibres over a locally Noetherian base; that route is unavailable here, and it would in any case be circular, since Tag 02OG rests on Tag 02OE above.

theorem exists_isFinite_morphismRestrict_of_finite_fibre {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsLocallyNoetherian Y] [IsProper f] (y : Y) (hfin : (f ⁻¹' {y}).Finite) :
    ∃ V : Y.Opens, y ∈ V ∧ IsFinite (f ∣_ V)

Tag 0D2M, a lemma

Tag 0D2M in the Stacks Project.

Stacks.FormalFunctions.exists_isZero_stalk_rightDerived_and_surjective_fiberTwist, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalFunctions/AmpleFibreTwistStalkSurjective.lean, line 701.

[Stacks, Tag 0D2M].

Let f : X ⟶ Y be a proper morphism of schemes with Y Noetherian, let ℒ be an invertible 𝒪_X-module, let ℱ be a coherent 𝒪_X-module and let y ∈ Y be a point such that ℒ_y is ample on the fibre X_y. Then there exists a d₀ such that for all d ≥ d₀

1. R ᵖ f_*(ℱ ⊗_{𝒪_X} ℒ ^⊗ d)_y = 0 for p > 0, and
2. the map f_*(ℱ ⊗_{𝒪_X} ℒ ^⊗ d)_y ⟶ H ⁰(X_y, ℱ_y ⊗_{𝒪_{X_y}} ℒ_y ^⊗ d) is surjective.

Here X_y is f.fiber y with its morphism f.fiberι y to X, ℱ_y and ℒ_y are the restrictions of ℱ and ℒ to it, R ᵖ f_* is the p-th right derived functor of Scheme.Modules.pushforward f, and H ⁰(X_y, -) is the module of global sections. The map in the second clause is Stacks.FormalFunctions.fiberTwistSectionsStalkHom: the germ at y of a section over f ⁻¹ U goes to its restriction to the fibre. The proof is exists_isZero_stalk_rightDerived_and_surjective_twistModule together with the identification (f.fiberι y) ^* (ℱ ⊗ ℒ ^⊗ d) ≅ ℱ_y ⊗ ℒ_y ^⊗ d of [Stacks, Tag 0EGK].

public theorem exists_isZero_stalk_rightDerived_and_surjective_fiberTwist (f : X ⟶ Y)
    [IsProper f] [AlgebraicGeometry.IsNoetherian Y] (y : Y) (F L : X.Modules)
    [IsInvertibleModule X L] [F.IsCoherent]
    (hL : IsAmple (f.fiber y) (pullbackModule (f.fiberι y) L)) :
    ∃ d₀ : ℤ, ∀ d : ℤ, d₀ ≤ d →
      (∀ p : ℕ, 0 < p →
          IsZero ((((Scheme.Modules.pushforward f).rightDerived p).obj
            (twistModule X L F d)).presheaf.stalk y)) ∧
        Function.Surjective (fiberTwistSectionsStalkHom f y F L d)

Tag 0D2N, a lemma

Tag 0D2N in the Stacks Project.

Stacks.AmpleFibreNeighbourhood.exists_mem_isRelativelyAmple_of_isAmple_fibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/AmpleFibreNeighbourhood/RelativelyAmpleNeighbourhood.lean, line 70.

Stacks Project, Tag 0D2N. Let f : X ⟶ Y be a proper morphism of schemes with Y Noetherian, let ℒ be an invertible 𝒪_X-module and let y be a point of Y such that ℒ_y is ample on the fibre X_y. Then there is an open neighbourhood V of y such that ℒ|_{f⁻¹V} is ample relative to f⁻¹V / V.

Invertibility of ℒ_y is not a hypothesis: it is an instance, the pullback of an invertible module being invertible (Stacks.InvertiblePullback.isInvertibleModule_pullback).

The two halves are Stacks.AmpleFibreNeighbourhood.exists_mem_pullbackSection_fiberι_eq — the lifting of sections from the fibre, which is where [Stacks, Tag 0D2M] and the reduction to Spec 𝒪_{Y, y} live — and Stacks.AmpleFibreNeighbourhood.exists_mem_isRelativelyAmple_of_exists_lift, which is the rest of the source's argument.

theorem exists_mem_isRelativelyAmple_of_isAmple_fibre {X S : Scheme.{u}} (f : X ⟶ S)
    [IsProper f] [IsNoetherian S] (L : X.Modules) [IsInvertibleModule X L] (y : S)
    (hL : IsAmple (f.fiber y) (pullbackModule (f.fiberι y) L)) :
    ∃ V : S.Opens, y ∈ V ∧
      Stacks.RelativeAmple.IsRelativelyAmple (f ∣_ V) (pullbackModule (f ⁻¹ᵁ V).ι L)

Sources

• Section 30.21, Tag 02OF
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.IsFinite.tfae_isProper_finite_preimage_singleton · Stacks.FormalFunctions.exists_isFinite_morphismRestrict_of_finite_fibre · Stacks.FormalFunctions.exists_isZero_stalk_rightDerived_and_surjective_fiberTwist · Stacks.AmpleFibreNeighbourhood.exists_mem_isRelativelyAmple_of_isAmple_fibre

Section30.22 Cohomology and base change, III#

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

Tag 07VK, a lemma

Tag 07VK in the Stacks Project.

Stacks.AlgebraicGeometry.ProperFlatGlobalSections.isPerfect_derivedGlobalSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ProperFlatGlobalSections.lean, line 644. The attribute's comment: “(1)”. References: SGA 6 0 (3.1), “affine-target flat case”; SGA 6 0 (4.1), “special case”; SGA 6 XIV (2.2), “special case”.

[Stacks, Tag 07VK] (1). Let A be a Noetherian ring, let f : X ⟶ Spec A be proper and let F be a coherent 𝒪_X-module flat over Spec A. Then RΓ(X, F) is a perfect object of D(A).

The proof is the source's. Properness makes X quasi-compact, so the affine open cover of X has a finite subcover 𝒰; properness also makes f separated, so the finite intersections of members of 𝒰 are affine. The alternating Čech complex of 𝒰 therefore computes RΓ(X, F) ([Stacks, Tag 01FM] and [Stacks, Tag 01ET]), is bounded, and is termwise flat over A ([Stacks, Tag 01U4]) — which is finite Tor dimension. Its cohomology modules are finite over A, which is [Stacks, Tag 02O6], so it is pseudo-coherent ([Stacks, Tag 066E]); [Stacks, Tag 0658] concludes.

Unconditional. The finiteness input — the affine-base case of [Stacks, Tag 02O5], carried through the lemmas above as the Prop AlgebraicGeometry.ProperCoherentImage.HigherDirectImageIsCoherentOverAffineBase — is supplied here by AlgebraicGeometry.ProperCoherenceWitness.higherDirectImageIsCoherentOverAffineBase, the hypothesis-free form of that tag. The finite-Tor-dimension half, hasFlatRepresentative_derivedGlobalSectionsOverBase, never needed it.

theorem isPerfect_derivedGlobalSections [IsNoetherianRing A] [IsProper f] [F.IsCoherent]
    (hflat : IsFlatOver f.toLRSHom.toShHom F) :
    StacksDraft.Perfect.IsPerfect (derivedGlobalSectionsOverBase f F)

Stacks.AlgebraicGeometry.ProperFlatGlobalSections.isIso_derivedGlobalSectionsBaseChangeMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ProperFlatGlobalSectionsBaseChange.lean, line 257. The attribute's comment: “(2), for the Čech base-change comparison of a finite affine cover”.

[Stacks, Tag 07VK] (2). Let φ : A ⟶ A' be a homomorphism of commutative rings, let f : X ⟶ Spec A be separated, let g : X' ⟶ X and f' : X' ⟶ Spec A' exhibit X' as the base change of X along Spec A' ⟶ Spec A, and let F be a quasi-coherent 𝒪_X-module flat over Spec A. Then the base-change map

RΓ(X, F) ⊗^L_A A' ⟶ RΓ(X', g^* F)

is an isomorphism in D(A').

The proof is the source's. The alternating Čech complex of a finite affine cover whose finite intersections are affine computes RΓ(X, F) ([Stacks, Tag 01FM] and [Stacks, Tag 01ET]), it is bounded, and flatness of F over the base makes it termwise flat ([Stacks, Tag 01U4]); for such a complex the ordinary extension of scalars is the derived one ([Stacks, Tag 06XY]), and the ordinary extension of scalars of the model is the model of the inverse-image cover on X' ([Stacks, Tag 01XL]), which computes RΓ(X', g^* F).

Unconditional. No Noetherian hypothesis, no properness, no coherence, and in particular no appeal to AlgebraicGeometry.ProperCoherentImage.HigherDirectImageIsCoherentOverAffineBase, which clause (1) threads and clause (2) does not need. The hypotheses are weaker than the source's: for A Noetherian, f proper and F coherent and flat they hold, a suitable cover being supplied by exists_finiteAffineCover_of_isProper.

theorem isIso_derivedGlobalSectionsBaseChangeMap
    (hflat : IsFlatOver f.toLRSHom.toShHom F) :
    IsIso (derivedGlobalSectionsBaseChangeMap φ hsq F U hU hUaff haff)

Tag 07VL, a remark

Tag 07VL in the Stacks Project.

Stacks.AlgebraicGeometry.ProperFlatGlobalSections.exists_finiteProjectiveModel_homology_iso_functorial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/ProperFlatGlobalSectionsFunctorialModel.lean, line 322. The attribute's comment: “Remark 30.22.2 in full: one bounded complex M of finite projective A-modules, the identification H^i(X_{A'}, F_{A'}) = H^i(M ⊗_A A') for every base change given as a family of isomorphisms indexed by the ring map, the cartesian square and the degree and pinned to the single chain-level model over A, and the functoriality in A' as the cocycle square for a second base change A' ⟶ A''; under exactly the source's conditions — A Noetherian, f proper, F coherent and flat over A — with the finite affine cover bound inside the existential and supplied by properness. The closing citation to Hartshorne that flatness is essential is remark-level and appears as documentation in the module docstring.”.

[Stacks, Tag 07VL], Remark 30.22.2, both clauses. Let A be a Noetherian ring, f : X ⟶ Spec A a proper morphism of schemes and F a coherent 𝒪_X-module flat over A. Then there is a bounded complex M of finite projective A-modules, a finite affine open cover of X whose finite intersections are affine, and a family of chain-level comparisons

Θ(φ, square) : M ⊗_A A' ⟶ Č_alt(g⁻¹U, g^* F)

indexed by a ring map φ : A ⟶ A' and a cartesian square exhibiting X' as the base change of X along Spec A' ⟶ Spec A, together with a family of identifications

c(φ, square, i) : Hⁱ(X', g^* F) ≅ Hⁱ(M ⊗_A A')

indexed also by the degree, such that

• every Θ(φ, square) is a quasi-isomorphism;
• c(φ, square, i) is the identification Θ(φ, square) induces on homology, so the family has a single origin over A and is not a choice per A';
• the comparisons are functorial in A': for a second ring map ψ : A' ⟶ A'' and a second cartesian square, the extension of scalars along ψ of Θ(φ, square), followed by the Čech base-change isomorphism for ψ and by the identification of the model of g'^* (g^* F) with that of (g' ≫ g)^* F, is Θ(ψ ∘ φ, pasted square) read through (M ⊗_A A') ⊗_{A'} A'' ≅ M ⊗_A A''.

The conditions are exactly the source's. Separatedness and quasi-coherence follow: properness gives the first and coherence the second. The cover is not an input either — it is bound inside the existential and produced by exists_finiteAffineCover_of_isProper — so the statement is about f and F alone.

The source's closing sentence, that flatness of F over A is essential with a reference to Hartshorne, has been ruled remark-level: it is a citation rather than a clause owing a theorem, and the module docstring records it as such.

theorem exists_finiteProjectiveModel_homology_iso_functorial [IsNoetherianRing A] [IsProper f]
    [F.IsCoherent] (hflat : IsFlatOver f.toLRSHom.toShHom F) :
    haveI : F.IsQuasicoherent := isQuasicoherent_of_isCoherent F
    ∃ (M : CochainComplex (ModuleCat.{u} A) ℤ) (a b : ℤ),
      M.IsStrictlyGE a ∧ M.IsStrictlyLE b ∧
        (∀ i : ℤ, Module.Finite A (M.X i)) ∧ (∀ i : ℤ, Module.Projective A (M.X i)) ∧
        ∃ (I : Type u) (hIfin : Finite I) (hIlin : LinearOrder I) (U : I → X.Opens)
          (hU : (⊤ : X.Opens) = ⨆ i, U i) (hUaff : ∀ i, IsAffineOpen (U i)),
          haveI : Finite I := hIfin
          letI : LinearOrder I := hIlin
          ∃ (_haff : ∀ (r : ℕ) (s : Fin (r + 1) → I), IsAffineOpen (⨅ k, U (s k)))
            (Θ : ∀ {A' : Type u} [CommRing A'] (φ : A →+* A') {X' : Scheme.{u}}
                {f' : X' ⟶ Spec (.of A')} {g : X' ⟶ X},
                IsPullback g f' f (Spec.map (CommRingCat.ofHom φ)) →
                  (extendScalarsComplex φ M ⟶
                    baseAlternatingCechComplex f' (fun j => g ⁻¹ᵁ U j)
                      (top_eq_iSup_preimage g U hU) ((Scheme.Modules.pullback g).obj F)))
            (c : ∀ {A' : Type u} [CommRing A'] (φ : A →+* A') {X' : Scheme.{u}}
                {f' : X' ⟶ Spec (.of A')} {g : X' ⟶ X}
                (_hsq : IsPullback g f' f (Spec.map (CommRingCat.ofHom φ))) (i : ℤ),
                ((DerivedCategory.homologyFunctor (ModuleCat.{u} A') i).obj
                    (derivedGlobalSectionsOverBase f' ((Scheme.Modules.pullback g).obj F)) ≅
                  (extendScalarsComplex φ M).homology i)),
            (∀ {A' : Type u} [CommRing A'] (φ : A →+* A') {X' : Scheme.{u}}
                {f' : X' ⟶ Spec (.of A')} {g : X' ⟶ X}
                (hsq : IsPullback g f' f (Spec.map (CommRingCat.ofHom φ))),
                QuasiIso (Θ φ hsq)) ∧
              (∀ {A' : Type u} [CommRing A'] (φ : A →+* A') {X' : Scheme.{u}}
                  {f' : X' ⟶ Spec (.of A')} {g : X' ⟶ X}
                  (hsq : IsPullback g f' f (Spec.map (CommRingCat.ofHom φ))) (i : ℤ),
                  (c φ hsq i).inv =
                    (DerivedCategory.homologyFunctorFactors (ModuleCat.{u} A') i).inv.app
                        (extendScalarsComplex φ M) ≫
                      (DerivedCategory.homologyFunctor (ModuleCat.{u} A') i).map
                        (DerivedCategory.Q.map (Θ φ hsq) ≫
                          (alternatingCechIsoDerivedGlobalSectionsOverBase f'
                            (fun j => g ⁻¹ᵁ U j) (top_eq_iSup_preimage g U hU)
                            ((Scheme.Modules.pullback g).obj F)
                            (iInf_preimage_isAffineOpen φ hsq U hUaff)).hom)) ∧
              (∀ {A' A'' : Type u} [CommRing A'] [CommRing A''] (φ : A →+* A') (ψ : A' →+* A'')
                  {X' X'' : Scheme.{u}} {f' : X' ⟶ Spec (.of A')} {f'' : X'' ⟶ Spec (.of A'')}
                  {g : X' ⟶ X} {g' : X'' ⟶ X'}
                  (hsq : IsPullback g f' f (Spec.map (CommRingCat.ofHom φ)))
                  (hsq' : IsPullback g' f'' f' (Spec.map (CommRingCat.ofHom ψ))),
                  haveI : IsSeparated f' := isSeparated_of_isPullback φ hsq
                  ((ModuleCat.extendScalars.{u, u, u} ψ).mapHomologicalComplex
                          (ComplexShape.up ℤ)).map (Θ φ hsq) ≫
                      (baseAlternatingCechComplexBaseChangeIso ψ hsq'
                          ((Scheme.Modules.pullback g).obj F) (fun j => g ⁻¹ᵁ U j)
                          (top_eq_iSup_preimage g U hU)
                          (isAffineOpen_preimage φ hsq U hUaff)).hom ≫
                      (baseAlternatingCechComplexMapIso f'' (fun j => (g' ≫ g) ⁻¹ᵁ U j)
                        (top_eq_iSup_preimage (g' ≫ g) U hU)
                        ((Scheme.Modules.pullbackComp g' g).app F)).hom =
                    (extendScalarsComplexCompIso φ ψ).hom.app M ≫
                      Θ (ψ.comp φ)
                        (Stacks.Cech.isPullback_comp_specMap φ ψ f f' f'' g g' hsq hsq'))

Sources

• Section 30.22, Tag 07VJ
• AxiomMath/Stacks at 5ed82d14

LeanStacks.AlgebraicGeometry.ProperFlatGlobalSections.isPerfect_derivedGlobalSections · Stacks.AlgebraicGeometry.ProperFlatGlobalSections.isIso_derivedGlobalSectionsBaseChangeMap · Stacks.AlgebraicGeometry.ProperFlatGlobalSections.exists_finiteProjectiveModel_homology_iso_functorial

Section30.23 Coherent formal modules#

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

Tag 087W, a lemma

Tag 087W in the Stacks Project.

Stacks.Coherent.coherentAdicSystemsEquivFGModuleCat, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CoherentAdicSystem/Equivalence.lean, line 541.

Stacks 087W. Coherent inverse systems on an affine Noetherian scheme are equivalent to finite modules over the completion of its ring of global sections.

public noncomputable def coherentAdicSystemsEquivFGModuleCat
    (X : Scheme.{u}) [IsAffine X] [IsNoetherianRing Γ(X, ⊤)]
    (I : Ideal Γ(X, ⊤)) :
    CoherentAdicSystems
      (Scheme.IdealSheafData.ofIdealTop I) ≌
        FGModuleCat.{u} (AdicCompletion I Γ(X, ⊤))

Stacks.Coherent.globalSectionsComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CoherentAdicSystem/Equivalence.lean, line 564. The attribute's comment: “inverse-limit object”.

Stacks 087W. The canonical comparison with the inverse limit of global sections.

public noncomputable def globalSectionsComparison
    (X : Scheme.{u}) [IsAffine X] [IsNoetherianRing Γ(X, ⊤)]
    (I : Ideal Γ(X, ⊤))
    (F : CoherentAdicSystems (Scheme.IdealSheafData.ofIdealTop I)) :
    completedModuleAsBase X I F ≅ limit (globalSectionsSystem F)

Stacks.Coherent.globalSectionsComparison_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CoherentAdicSystem/Equivalence.lean, line 581. The attribute's comment: “naturality”.

Stacks 087W. The comparison is natural in morphisms of coherent adic systems.

public theorem globalSectionsComparison_naturality
    (X : Scheme.{u}) [IsAffine X] [IsNoetherianRing Γ(X, ⊤)]
    (I : Ideal Γ(X, ⊤))
    {F G : CoherentAdicSystems (Scheme.IdealSheafData.ofIdealTop I)}
    (f : F ⟶ G) :
    (ModuleCat.restrictScalars (algebraMap Γ(X, ⊤)
      (AdicCompletion I Γ(X, ⊤)))).map
        ((coherentAdicSystemsEquivFGModuleCat X I).functor.map f).hom ≫
      (globalSectionsComparison X I G).hom =
    (globalSectionsComparison X I F).hom ≫
      limMap (F := globalSectionsSystem F) (G := globalSectionsSystem G)
        (Functor.whiskerRight f.hom
        (SheafOfModules.evaluation X.ringCatSheaf (op ⊤)))

Stacks.Coherent.globalSectionsComparison_projection_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CoherentAdicSystem/Equivalence.lean, line 616. The attribute's comment: “surjective projections”.

Stacks 087W. Projection from the corresponding completed module onto any term is surjective.

public theorem globalSectionsComparison_projection_surjective
    (X : Scheme.{u}) [IsAffine X] [IsNoetherianRing Γ(X, ⊤)]
    (I : Ideal Γ(X, ⊤))
    (F : CoherentAdicSystems (Scheme.IdealSheafData.ofIdealTop I))
    (n : ℕ) :
    Function.Surjective
      (((globalSectionsComparison X I F).hom ≫
        limit.π (globalSectionsSystem F) (op n)).hom)

Stacks.Coherent.globalSectionsComparison_projection_ker, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CoherentAdicSystem/Equivalence.lean, line 631. The attribute's comment: “canonical quotient”.

Stacks 087W. The kernel of the projection is exactly the (n+1)-st ideal power multiple, so the induced map from the quotient is an isomorphism.

public theorem globalSectionsComparison_projection_ker
    (X : Scheme.{u}) [IsAffine X] [IsNoetherianRing Γ(X, ⊤)]
    (I : Ideal Γ(X, ⊤))
    (F : CoherentAdicSystems (Scheme.IdealSheafData.ofIdealTop I))
    (n : ℕ) :
    LinearMap.ker
      (((globalSectionsComparison X I F).hom ≫
        limit.π (globalSectionsSystem F) (op n)).hom) =
      I ^ (n + 1) • (⊤ : Submodule Γ(X, ⊤) (completedModuleAsBase X I F))

Tag 087X, a lemma

Tag 087X in the Stacks Project.

Stacks.Coherent.abelian_coherentAdicSystems, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CoherentAdicSystem/Abelian.lean, line 200. The attribute's comment: “the category is abelian”.

Part (1) of Tag 087X: the category of coherent adic systems on a Noetherian scheme is abelian. It is preadditive, has kernels, cokernels and finite products, and its coimage-image comparisons are invertible.

public instance abelian_coherentAdicSystems {X : Scheme.{u}} [IsNoetherian X]
    (I : X.IdealSheafData) : Abelian (CoherentAdicSystems I)

Stacks.Coherent.restrictFunctor_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CoherentAdicSystem/Abelian.lean, line 208. The attribute's comment: “restriction to an open is exact”.

Part (2) of Tag 087X: restriction to an open subscheme is exact on coherent adic systems. Restriction preserves finite limits, being compatible with the kernel construction, and finite colimits, being a left adjoint computed termwise.

public theorem restrictFunctor_exact {X : Scheme.{u}} [IsNoetherian X] (I : X.IdealSheafData)
    {Y : Scheme.{u}} (f : Y ⟶ X) [IsOpenImmersion f] :
    PreservesFiniteLimits (restrictFunctor I f) ∧
      PreservesFiniteColimits (restrictFunctor I f)

Stacks.Coherent.exact_iff_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CoherentAdicSystem/ExactnessLocal.lean, line 133. The attribute's comment: “exactness may be checked on an open covering”.

Part (3) of Tag 087X: exactness in Coh(X, ℐ) may be checked on an open covering of X. A pair of morphisms α : F ⟶ G and β : G ⟶ H of coherent adic systems on a Noetherian scheme is an exact sequence if and only if, for every member U j of an open covering of X, the restrictions of α and β to U j form an exact sequence.

Both the condition that the composite vanish and the exactness of the resulting short complex are local.

public theorem exact_iff_restrict {X : Scheme.{u}} [IsNoetherian X] (I : X.IdealSheafData)
    {F G H : CoherentAdicSystems I} (α : F ⟶ G) (β : G ⟶ H)
    {J : Type v} (U : J → X.Opens) (hU : iSup U = ⊤) :
    (∃ h : α ≫ β = 0, (ShortComplex.mk α β h).Exact) ↔
      ∀ j : J, ∃ h : (restrictFunctor I (U j).ι).map α ≫ (restrictFunctor I (U j).ι).map β = 0,
        (ShortComplex.mk ((restrictFunctor I (U j).ι).map α)
          ((restrictFunctor I (U j).ι).map β) h).Exact

Tag 087Y, a lemma

Tag 087Y in the Stacks Project.

Stacks.Coherent.epi_iff_epi_app_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CoherentAdicSystem/Epi.lean, line 65.

Stacks 087Y. A morphism of coherent adic systems is surjective exactly when its component at the lowest level is surjective.

public theorem epi_iff_epi_app_zero {F G : CoherentAdicSystems I} (f : F ⟶ G) :
    Epi f ↔ Epi (f.hom.app (op 0))

Tag 0880, an equation

Tag 0880 in the Stacks Project.

Stacks.Algebraization.completionFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionFunctor/Basic.lean, line 475. The attribute's comment: “the functor”.

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

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

Stacks.Algebraization.completionFunctor_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionFunctor/Basic.lean, line 488. The attribute's comment: “object formula”.

The n-th term of the completion is the quotient by I ^ (n+1).

public theorem completionFunctor_obj (X : Scheme.{u})
    [AlgebraicGeometry.IsLocallyNoetherian X] (I : X.IdealSheafData)
    (F : AlgebraicGeometry.SheafOfModules.CoherentModules X.ringCatSheaf) (n : ℕ) :
    ((completionFunctor X I).obj F).obj.obj (op n) = idealPowerQuotient I (n + 1) F.obj

Stacks.Algebraization.completionProjection_transition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionFunctor/Basic.lean, line 504. The attribute's comment: “transition maps”.

The projections are compatible with the transition maps of the inverse system.

public theorem completionProjection_transition (X : Scheme.{u})
    [AlgebraicGeometry.IsLocallyNoetherian X] (I : X.IdealSheafData)
    (F : AlgebraicGeometry.SheafOfModules.CoherentModules X.ringCatSheaf) (n : ℕ) :
    completionProjection X I F (n + 1) ≫
        ((completionFunctor X I).obj F).obj.map (homOfLE (Nat.le_succ n)).op =
      completionProjection X I F n

Stacks.Algebraization.completionFunctor_map_quotient, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionFunctor/Basic.lean, line 515. The attribute's comment: “morphism maps”.

Completion maps are exactly the maps induced on the successive quotients.

public theorem completionFunctor_map_quotient (X : Scheme.{u})
    [AlgebraicGeometry.IsLocallyNoetherian X] (I : X.IdealSheafData)
    {F G : AlgebraicGeometry.SheafOfModules.CoherentModules X.ringCatSheaf} (f : F ⟶ G) (n : ℕ) :
    completionProjection X I F n ≫ ((completionFunctor X I).map f).hom.app (op n) =
      f.hom ≫ completionProjection X I G n

Tag 0881, a lemma

Tag 0881 in the Stacks Project.

Stacks.Algebraization.completionFunctor_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionFunctor/Exactness.lean, line 389.

Stacks 0881: the completion functor Coh(𝒪_X) ⥤ Coh(X, I) of Stacks 0880 is exact.

It is right exact because the completion of a coherent module is a quotient construction, and it preserves monomorphisms by Artin–Rees; a right exact functor between abelian categories which preserves monomorphisms is exact.

public theorem completionFunctor_exact :
    exactFunctor _ _ (completionFunctor X I)

Tag 0882, a lemma

Tag 0882 in the Stacks Project.

Stacks.Algebraization.completionInternalHomEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionFunctor/InternalHomCompletion.lean, line 228. References: SGA 2 X (2.2), “partial”.

Stacks 0882. Let X be a locally Noetherian scheme, I a quasi-coherent sheaf of ideals on X and G, F coherent 𝒪_X-modules; put H = SheafHom(G, F). Then

lim_n H⁰(X, H / Iⁿ H) = Mor_{Coh(X, I)}(G^∧, F^∧).

The left side is the inverse limit of the global sections of the completion of the internal hom; the right side the morphisms of coherent adic systems between the completions of G and F. The identification is additive.

Four steps: global sections commute with the inverse limit; the comparison lim H / Iⁿ H ⟶ SheafHom(G, lim F / Iⁿ F) is an isomorphism (isIso_completedSheafHomComparison); the global sections of an internal hom are the morphisms (internalHomSectionsTopEquiv); and a morphism G ⟶ lim F / Iⁿ F is a morphism of coherent adic systems G^∧ ⟶ F^∧ (completionHomLimitEquiv).

Stacks states this for a Noetherian scheme; it holds, as here, on any locally Noetherian one.

public noncomputable def completionInternalHomEquiv (X : Scheme.{u}) [IsLocallyNoetherian X]
    (I : X.IdealSheafData)
    (G F : AlgebraicGeometry.SheafOfModules.CoherentModules X.ringCatSheaf) :
    limit (C := ModuleCat.{u} Γ(X, ⊤)) (Stacks.Coherent.globalSectionsSystem
      ((completionFunctor X I).obj (internalHomCoherent X G F))) ≃+
      ((completionFunctor X I).obj G ⟶ (completionFunctor X I).obj F)

Tag 0889, a lemma

Tag 0889 in the Stacks Project.

Stacks.Algebraization.exists_unique_algebraization_of_isNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/Algebraize.lean, line 863. The attribute's comment: “part (1): algebraization of a map into a completion”.

Stacks 0889 (1) on a Noetherian scheme. Let X be a Noetherian scheme, ℐ a quasi-coherent ideal sheaf, G a coherent 𝒪_X-module and (F_n) a coherent ℐ-adic system. A morphism α : (F_n) ⟶ G^∧ whose levelwise kernels and cokernels are annihilated by a power of ℐ admits a triple (F, a, β), unique up to a unique isomorphism, with F a coherent 𝒪_X-module, a : F ⟶ G a morphism whose kernel and cokernel are annihilated by a power of ℐ, β : (F_n) ≅ F^∧ an isomorphism, and α = a^∧ ∘ β. Uniqueness: for a second such triple (F', a', β') there is exactly one isomorphism d : F ≅ F' of triples, that is, with a' ∘ d = a and d^∧ ∘ β = β'.

The existence is Stacks.Algebraization.exists_unique_algebraization with its one premise supplied by Stacks.Algebraization.isPowerAnnihilated_of_restrict: on a Noetherian scheme the affine-local annihilation of a sheaf of modules by powers of ℐ|_U is annihilation by a single power of ℐ, because quasi-compactness extracts a finite affine covering and annihilation by a fixed power is local on the base. The uniqueness there is read on lim (F_n), and completionMap_comp_eq_iff_limMap turns it into the compatibility d^∧ ∘ β = β'. The conditions are exactly those of the source.

public theorem exists_unique_algebraization_of_isNoetherian {X : Scheme.{u}} [IsNoetherian X]
    (I : X.IdealSheafData)
    (G : AlgebraicGeometry.SheafOfModules.CoherentModules X.ringCatSheaf)
    (Fsys : Stacks.Coherent.CoherentAdicSystems I)
    (α : Fsys.obj ⟶ ((completionFunctor X I).obj G).obj)
    (hα : IsKernelCokernelAnnihilatedByPower I α) :
    ∃ (F : AlgebraicGeometry.SheafOfModules.CoherentModules X.ringCatSheaf) (a : F ⟶ G)
      (β : Fsys.obj ≅ ((completionFunctor X I).obj F).obj),
      (α = β.hom ≫ ((completionFunctor X I).map a).hom ∧
          IsPowerAnnihilated I (kernel (C := X.Modules) a.hom) ∧
            IsPowerAnnihilated I (cokernel (C := X.Modules) a.hom)) ∧
        ∀ (F' : AlgebraicGeometry.SheafOfModules.CoherentModules X.ringCatSheaf) (a' : F' ⟶ G)
            (β' : Fsys.obj ≅ ((completionFunctor X I).obj F').obj),
          α = β'.hom ≫ ((completionFunctor X I).map a').hom →
            IsPowerAnnihilated I (kernel (C := X.Modules) a'.hom) →
              IsPowerAnnihilated I (cokernel (C := X.Modules) a'.hom) →
                ∃! d : F ≅ F',
                  d.hom ≫ a' = a ∧
                    β.hom ≫ ((completionFunctor X I).map d.hom).hom = β'.hom

Stacks.Algebraization.exists_unique_algebraization_dual_of_isNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizeDualTheorem.lean, line 395. The attribute's comment: “part (2): algebraization of a map out of a completion”.

Stacks 0889 (2). Let X be a Noetherian scheme, ℐ a quasi-coherent ideal sheaf, G a coherent 𝒪_X-module and (F_n) a coherent ℐ-adic system. A morphism α : G^∧ ⟶ (F_n) whose levelwise kernels and cokernels are annihilated by a power of ℐ admits a triple (F, a, β), unique up to a unique isomorphism, with F a coherent 𝒪_X-module, a : G ⟶ F a morphism whose kernel and cokernel are annihilated by a power of ℐ, β : F^∧ ≅ (F_n) an isomorphism, and α = β ∘ a^∧.

The existence is Stacks.Algebraization.exists_algebraization_dual, whose affine-local annihilation of the kernel and the cokernel of a becomes annihilation by a single power of ℐ by Stacks.Algebraization.isPowerAnnihilated_of_restrict, using that X is quasi-compact. The uniqueness is Stacks.Algebraization.unique_algebraization_dual.

public theorem exists_unique_algebraization_dual_of_isNoetherian {X : Scheme.{u}}
    [IsNoetherian X] (I : X.IdealSheafData)
    (G : AlgebraicGeometry.SheafOfModules.CoherentModules X.ringCatSheaf)
    (Fsys : Stacks.Coherent.CoherentAdicSystems I)
    (α : ((completionFunctor X I).obj G).obj ⟶ Fsys.obj)
    (hα : IsKernelCokernelAnnihilatedByPower I α) :
    ∃ (F : AlgebraicGeometry.SheafOfModules.CoherentModules X.ringCatSheaf) (a : G ⟶ F)
      (β : ((completionFunctor X I).obj F).obj ≅ Fsys.obj),
      (α = ((completionFunctor X I).map a).hom ≫ β.hom ∧
          IsPowerAnnihilated I (kernel (C := X.Modules) a.hom) ∧
            IsPowerAnnihilated I (cokernel (C := X.Modules) a.hom)) ∧
        ∀ (F' : AlgebraicGeometry.SheafOfModules.CoherentModules X.ringCatSheaf) (a' : G ⟶ F')
            (β' : ((completionFunctor X I).obj F').obj ≅ Fsys.obj),
          α = ((completionFunctor X I).map a').hom ≫ β'.hom →
            IsPowerAnnihilated I (kernel (C := X.Modules) a'.hom) →
              IsPowerAnnihilated I (cokernel (C := X.Modules) a'.hom) →
                ∃! d : F ≅ F',
                  a ≫ d.hom = a' ∧
                    ((completionFunctor X I).map d.hom).hom ≫ β'.hom = β.hom

Tag 0EHP, a lemma

Tag 0EHP in the Stacks Project.

Stacks.Algebraization.essImage_and_bijective_of_isPowerAnnihilated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionFunctor/TorsionExtBijective.lean, line 532.

[Stacks, Tag 0EHP]. Let X be a Noetherian scheme and ℐ ⊂ 𝒪_X a quasi-coherent sheaf of ideals.

• Any object of Coh(X, ℐ) annihilated by a power of ℐ is in the essential image of the completion functor of Stacks 0880.
• If ℱ, 𝒢 are coherent 𝒪_X-modules and a power of ℐ annihilates ℱ or 𝒢, then both

Hom_X(ℱ, 𝒢) ⟶ Hom_{Coh(X, ℐ)}(ℱ^∧, 𝒢^∧) and Ext_X(ℱ, 𝒢) ⟶ Ext_{Coh(X, ℐ)}(ℱ^∧, 𝒢^∧)

are isomorphisms.

Both comparison maps are the ones induced by the completion functor, and both are homomorphisms of abelian groups for formal reasons — the functor is additive — so their bijectivity is the whole of the source's assertion that they are isomorphisms.

public theorem essImage_and_bijective_of_isPowerAnnihilated (X : Scheme.{u}) [IsNoetherian X]
    (I : X.IdealSheafData) :
    (∀ S : Stacks.Coherent.CoherentAdicSystems I, IsSystemPowerAnnihilated I S.obj →
        (completionFunctor X I).essImage S) ∧
      ∀ F G : AlgebraicGeometry.SheafOfModules.CoherentModules X.ringCatSheaf,
        IsPowerAnnihilated I F.obj ∨ IsPowerAnnihilated I G.obj →
          Function.Bijective (fun f : F ⟶ G => (completionFunctor X I).map f) ∧
            Function.Bijective ((completionFunctor X I).mapExtAddHom F G 1)

Tag 087Z, a lemma

Tag 087Z in the Stacks Project.

Stacks.Coherent.finiteTypeAssociatedGradedData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CoherentAdicSystem/AssociatedGraded/GradedModuleFiniteType.lean, line 670.

Stacks Project, Tag 087Z. For a Noetherian scheme X and a quasi-coherent sheaf of ideals ℐ, the transition kernels of an object of Coh(X, ℐ) form a finite type, graded, quasi-coherent module over the associated graded algebra ⨁ ℐ ⁿ / ℐ ⁿ⁺¹.

public theorem finiteTypeAssociatedGradedData {X : Scheme.{u}} [IsNoetherian X]
    (I : X.IdealSheafData) (F : CoherentAdicSystems I) :
    Nonempty (AssociatedGradedData I F)

Tag 0887, a lemma

Tag 0887 in the Stacks Project.

Stacks.Coherent.coherentAdicPullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CoherentAdicSystem/Pullback.lean, line 200. The attribute's comment: “the functor f^*”.

Stacks 0887: the functor f^* : Coh(Y, 𝒥) ⟶ Coh(X, ℐ). For a morphism f : X ⟶ Y of Noetherian schemes and a quasi-coherent sheaf of ideals 𝒥 on Y, termwise pullback is a functor from the coherent adic systems along 𝒥 to those along ℐ = f^{-1}𝒥 𝒪_X.

It is built as a lift of termwise pullback, so its action on objects and morphisms is the canonical one; see Stacks.Coherent.coherentAdicPullback_obj_obj.

public def coherentAdicPullback {X Y : Scheme.{u}} [IsNoetherian X] [IsNoetherian Y]
    (f : X ⟶ Y) (J : Y.IdealSheafData) :
    CoherentAdicSystems J ⥤ CoherentAdicSystems (J.comap f)

Stacks.Coherent.coherentAdicPullback_obj_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CoherentAdicSystem/Pullback.lean, line 210. The attribute's comment: “the functor sends (G n) to (f^* G n)”.

The functor of Stacks 0887 sends the system (G_n) to the system (f^*G_n).

public theorem coherentAdicPullback_obj_obj {X Y : Scheme.{u}} [IsNoetherian X] [IsNoetherian Y]
    (f : X ⟶ Y) (J : Y.IdealSheafData) (G : CoherentAdicSystems J) (n : ℕᵒᵖ) :
    ((coherentAdicPullback f J).obj G).obj.obj n =
      (Scheme.Modules.pullback f).obj (G.obj.obj n)

Stacks.Coherent.coherentAdicPullback_rightExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CoherentAdicSystem/Pullback.lean, line 233. The attribute's comment: “right exactness”.

Stacks 0887: the pullback functor on coherent adic systems is right exact.

Termwise pullback of inverse systems preserves all colimits, being a left adjoint; the inclusion of Coh(Y, 𝒥) preserves finite colimits, cokernels there being levelwise; so the composite of f^* with the inclusion of Coh(X, ℐ) preserves finite colimits, and that inclusion reflects them.

public theorem coherentAdicPullback_rightExact {X Y : Scheme.{u}} [IsNoetherian X]
    [IsNoetherian Y] (f : X ⟶ Y) (J : Y.IdealSheafData) :
    rightExactFunctor _ _ (coherentAdicPullback f J)

Stacks.Coherent.coherentAdicPullback_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CoherentAdicSystem/Pullback.lean, line 351. The attribute's comment: “exactness when f is flat”.

Stacks 0887: along a flat morphism the pullback functor on coherent adic systems is exact.

public theorem coherentAdicPullback_exact {X Y : Scheme.{u}} [IsNoetherian X] [IsNoetherian Y]
    (f : X ⟶ Y) (J : Y.IdealSheafData) [Flat f] :
    exactFunctor _ _ (coherentAdicPullback f J)

Tag 0EHQ, a lemma

Tag 0EHQ in the Stacks Project.

Stacks.Coherent.coherentAdicPullback_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CoherentAdicSystem/PullbackEquivalence.lean, line 737.

[Stacks, Tag 0EHQ]. Let f : X ⟶ Y be a flat morphism of Noetherian schemes, let 𝒥 ⊆ 𝒪_Y be a quasi-coherent sheaf of ideals cutting out Z ⊆ Y, and let ℐ = 𝒥.comap f ⊆ 𝒪_X cut out the scheme-theoretic inverse image Z' = f^{-1}Z. If the induced morphism Z' ⟶ Z is an isomorphism, then the pullback functor

f^* : Coh(Y, 𝒥) ⟶ Coh(X, ℐ)

of [Stacks, Tag 0887] is an equivalence.

The functor is left adjoint to the termwise direct image coherentAdicPushforward, which is an equivalence, and a left adjoint of an equivalence is an equivalence.

public theorem coherentAdicPullback_isEquivalence {X Y : Scheme.{u}} [IsNoetherian X]
    [IsNoetherian Y] (f : X ⟶ Y) [Flat f] (J : Y.IdealSheafData)
    [IsIso ((J.comapIso f).hom ≫ pullback.snd f J.subschemeι)] :
    (coherentAdicPullback f J).IsEquivalence

Tag 0EHR, a lemma

Tag 0EHR in the Stacks Project.

Stacks.Coherent.coherentAdicSystemsEquivOfSupportEq, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CoherentAdicSystem/IdealChange.lean, line 616.

[Stacks, Tag 0EHR]. Let X be a Noetherian scheme and let ℐ, 𝒥 ⊆ 𝒪_X be quasi-coherent sheaves of ideals. If V(ℐ) = V(𝒥) as closed subsets of X, then the categories Coh(X, ℐ) and Coh(X, 𝒥) of coherent adic inverse systems are equivalent.

Equal supports give positive exponents with ℐ ᵃ ⊆ 𝒥 and 𝒥 ᵇ ⊆ ℐ, and the two transfer functors they define are mutually quasi-inverse.

public def coherentAdicSystemsEquivOfSupportEq (X : Scheme.{u}) [IsNoetherian X]
    (I J : X.IdealSheafData) (h : I.support = J.support) :
    CoherentAdicSystems I ≌ CoherentAdicSystems J

Sources

• Section 30.23, Tag 0EHN
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Coherent.coherentAdicSystemsEquivFGModuleCat · Stacks.Coherent.globalSectionsComparison · Stacks.Coherent.globalSectionsComparison_naturality · Stacks.Coherent.globalSectionsComparison_projection_surjective · Stacks.Coherent.globalSectionsComparison_projection_ker · Stacks.Coherent.abelian_coherentAdicSystems · Stacks.Coherent.restrictFunctor_exact · Stacks.Coherent.exact_iff_restrict

Section30.24 Grothendieck's existence theorem, I#

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

Tag 0883, a lemma

Tag 0883 in the Stacks Project.

Stacks.Algebraization.fullyFaithful_completionFunctor_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionFunctor/FullyFaithfulComplete.lean, line 283.

Stacks 0883. Let A be a Noetherian ring complete with respect to an ideal J, let f : X ⟶ Spec A be proper and let 𝓙 = J · 𝒪_X. Then the completion functor Coh(𝒪_X) ⥤ Coh(X, 𝓙) of Stacks 0880 is fully faithful.

public theorem fullyFaithful_completionFunctor_of_isProper :
    letI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian f
    Nonempty (completionFunctor X (baseIdealSheaf A J f)).FullyFaithful

Tag 0884, a lemma

Tag 0884 in the Stacks Project.

Stacks.Coherent.exists_isZero_Hgroup_transitionKernel_tensorPowModule_of_isRelativelyAmple, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CoherentAdicSystem/TransitionKernelTwistVanishingAmple.lean, line 73.

Stacks 0884. Let A be a Noetherian ring, I ⊆ A an ideal, f : X ⟶ Spec A a proper morphism and L an invertible 𝒪_X-module ample relative to f. Let 𝓕 be an object of Coh(X, 𝓘) for 𝓘 = I · 𝒪_X. Then there is an integer d₀ such that

H¹(X, Ker(𝓕_{n+1} ⟶ 𝓕_n) ⊗ L ^⊗ d) = 0

for every n ≥ 0 and every d ≥ d₀ — one d₀ for the whole system.

The hypotheses are exactly the source's. The proof is the degree-one case of Stacks.Coherent.exists_isZero_Hgroup_transitionKernel_tensorPowModule_of_pos (Stacks 087Z and Stacks 0897 part (2)), whose ampleness hypothesis on V(𝓘) follows from f-ampleness by Stacks 01VK over the affine base and Stacks 0892 part (2) along the closed immersion V(𝓘) ⟶ X.

public theorem exists_isZero_Hgroup_transitionKernel_tensorPowModule_of_isRelativelyAmple
    (A : Type u) [CommRing A] [IsNoetherianRing A] (I : Ideal A)
    {X : Scheme.{u}} (f : X ⟶ Spec (.of A)) [IsProper f]
    (L : X.Modules) [Stacks.Ample.IsInvertibleModule X L]
    (hL : Stacks.RelativeAmple.IsRelativelyAmple f L)
    (𝓕 : CoherentAdicSystems (baseIdealSheaf A I f)) :
    ∃ d₀ : ℤ, ∀ (n : ℕ) (d : ℤ), d₀ ≤ d →
      IsZero (Hgroup X.ringCatSheaf ⊤ 1
        ((((Stacks.SheafOfModules.Tensor.sheafTensor ⟨X.presheaf,
              Presheaf.isSheaf_of_isSheaf_comp _ (X.presheaf) (forget₂ CommRingCat RingCat)
                ((isSheaf_structureRingPresheaf X))⟩).obj (transitionKernel 𝓕 n)).obj
          (Stacks.Ample.tensorPowModule X L d))))

Tag 0885, a lemma

Tag 0885 in the Stacks Project.

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

Grothendieck's existence theorem for a projective morphism, [Stacks, Tag 0885], read at clause (1) of Tag 01W8.

Let A be a Noetherian ring complete with respect to I, let f : X ⟶ Spec A be projective — a closed immersion over Spec A into a projective bundle 𝐏(ℰ) — and set 𝓘 = I · 𝒪_X. Then the completion functor Coh(𝒪_X) ⥤ Coh(X, 𝓘) of Stacks 0880 is an equivalence.

Nothing is assumed beyond the source's hypotheses. In particular UniversallyClosed f and LocallyOfFiniteType f are derived from projectivity, through AlgebraicGeometry.IsProjective.isProper, rather than assumed; so is the local Noetherianity of X that the completion functor of Stacks 0880 needs, and so is the f-ample invertible module L the proof chooses.

Full faithfulness is Stacks 0883 (Stacks.Algebraization.fullyFaithful_completionFunctor_of_isProper). Essential surjectivity is Stacks.Algebraization.essSurj_of_forall_exists_epi fed by the generation statement Stacks.Algebraization.exists_epi_completionFunctor_of_vanishing, whose own input is the uniform H¹-vanishing of Stacks 0884 (Stacks.Coherent.exists_isZero_Hgroup_transitionKernel_tensorPowModule); and that theorem's single hypothesis, part (2) of Stacks 0897 for the associated graded algebra of 𝓘, is Stacks.Coherent.hasAssociatedGradedTwistVanishing_of_isProper, which needs only properness and the invertibility of L.

The name's _of_vanishing records the shape the statement had while that hypothesis was still carried; it is kept because the statement itself did not change.

public theorem isEquivalence_completionFunctor_of_isProjective_of_vanishing
    (hf : AlgebraicGeometry.IsProjective f) :
    letI : IsProper f := hf.isProper
    letI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian f
    (completionFunctor X (baseIdealSheaf A I f)).IsEquivalence

Sources

• Section 30.24, Tag 087V
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Algebraization.fullyFaithful_completionFunctor_of_isProper · Stacks.Coherent.exists_isZero_Hgroup_transitionKernel_tensorPowModule_of_isRelativelyAmple · Stacks.Algebraization.isEquivalence_completionFunctor_of_isProjective_of_vanishing

Section30.25 Grothendieck's existence theorem, II#

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

Tag 0888, a remark

Tag 0888 in the Stacks Project.

Ideal.existsUnique_canonicalMap_of_smul_eq_bot, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/Annihilator.lean, line 114. The attribute's comment: “canonical_fg_map”.

Stacks Project, Tag 0888. In an exact sequence whose two end modules are annihilated by an ideal I, elements f, g ∈ I determine a unique linear map N → M. Its value at y is g • x for any lift x of f • y, and its composite with M → N is multiplication by f * g.

theorem existsUnique_canonicalMap_of_smul_eq_bot
    (i : T →ₗ[A] M) (a : M →ₗ[A] N) (q : N →ₗ[A] Q)
    (hia : Function.Exact i a) (haq : Function.Exact a q)
    (I : Ideal A)
    (hT : I • (⊤ : Submodule A T) = ⊥)
    (hQ : I • (⊤ : Submodule A Q) = ⊥)
    {f g : A} (hf : f ∈ I) (hg : g ∈ I) :
    ∃! b : N →ₗ[A] M,
      (∀ (y : N) (x : M), a x = f • y → b y = g • x) ∧
        b.comp a = LinearMap.lsmul A M (f * g)

Ideal.pow_le_annihilator_ker_mapQ_of_exact, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/Annihilator.lean, line 154. The attribute's comment: “annihilation_mod_ideal”.

Stacks Project, Tag 0888. In an exact five-term sequence whose end modules are annihilated by K ^ t, the power K ^ (2 * t) annihilates the kernel of the map induced after reduction modulo any ideal J.

lemma pow_le_annihilator_ker_mapQ_of_exact
    (i : T →ₗ[A] M) (a : M →ₗ[A] N) (q : N →ₗ[A] Q)
    (_hi : Function.Injective i) (hia : Function.Exact i a)
    (haq : Function.Exact a q) (_hq : Function.Surjective q)
    (K : Ideal A) (t : ℕ) (_ht : 0 < t)
    (hT : K ^ t ≤ Module.annihilator A T)
    (hQ : K ^ t ≤ Module.annihilator A Q) (J : Ideal A) :
    K ^ (2 * t) ≤ Module.annihilator A
      ↑(LinearMap.ker (Submodule.mapQ (J • (⊤ : Submodule A M))
        (J • (⊤ : Submodule A N)) a
        (Submodule.smul_top_le_comap_smul_top J a)))

Ideal.pow_le_annihilator_coker_mapQ_of_exact, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/Annihilator.lean, line 196. The attribute's comment: “annihilation_mod_ideal”.

Stacks Project, Tag 0888. In an exact five-term sequence whose end modules are annihilated by K ^ t, the power K ^ (2 * t) annihilates the cokernel of the map induced after reduction modulo any ideal J.

lemma pow_le_annihilator_coker_mapQ_of_exact
    (i : T →ₗ[A] M) (a : M →ₗ[A] N) (q : N →ₗ[A] Q)
    (_hi : Function.Injective i) (_hia : Function.Exact i a)
    (haq : Function.Exact a q) (_hq : Function.Surjective q)
    (K : Ideal A) (t : ℕ) (_ht : 0 < t)
    (_hT : K ^ t ≤ Module.annihilator A T)
    (hQ : K ^ t ≤ Module.annihilator A Q) (J : Ideal A) :
    K ^ (2 * t) ≤ Module.annihilator A
      (_ ⧸ LinearMap.range
        (Submodule.mapQ (J • (⊤ : Submodule A M)) (J • (⊤ : Submodule A N)) a
          (Submodule.smul_top_le_comap_smul_top J a)))

Stacks.Algebraization.idealPowerMultiple_kernel_cokernel_idealPowerQuotientMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/Coherent/AnnihilatorSheaf.lean, line 255. The attribute's comment: “annihilation_mod_ideal, over sheaves of modules”.

Let a : M ⟶ N be a morphism of quasi-coherent 𝒪_X-modules whose kernel and cokernel are annihilated by 𝒦 ᵗ, and let ℐ be any quasi-coherent ideal sheaf. Then 𝒦 ²ᵗ annihilates both the kernel and the cokernel of the induced map M / ℐ ⁿ M ⟶ N / ℐ ⁿ N.

This is the sheaf-of-modules form of Ideal.pow_le_annihilator_ker_mapQ_of_exact and Ideal.pow_le_annihilator_coker_mapQ_of_exact.

public theorem idealPowerMultiple_kernel_cokernel_idealPowerQuotientMap
    (I K : X.IdealSheafData) {M N : X.Modules} [M.IsQuasicoherent] [N.IsQuasicoherent]
    (a : M ⟶ N) {t : ℕ}
    (hk : idealPowerMultiple K t (kernel (C := X.Modules) a) = ⊥)
    (hc : idealPowerMultiple K t (cokernel (C := X.Modules) a) = ⊥) (n : ℕ) :
    idealPowerMultiple K (2 * t)
        (kernel (C := X.Modules) (idealPowerQuotientMap I I n n le_rfl a)) = ⊥ ∧
      idealPowerMultiple K (2 * t)
        (cokernel (C := X.Modules) (idealPowerQuotientMap I I n n le_rfl a)) = ⊥

Stacks.Algebraization.isKernelCokernelAnnihilatedByPower_iff_affine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AnnihilatedAffineCriterion.lean, line 516. The attribute's comment: “equivalence of (1) and (2) on an affine scheme”.

Stacks Project, Tag 0888, conditions (1) and (2) on an affine scheme. For a morphism α of Coh(Y, 𝓘) on an affine Noetherian scheme Y the following are equivalent: one positive power of 𝓚 annihilates every levelwise kernel Ker(α_n) and every levelwise cokernel Coker(α_n); and one positive power of K = 𝓚(⊤) annihilates the kernel and the cokernel of the map α_Y : M → N of finite modules over the completion which Tag 087W attaches to α.

Both ideal sheaves on an affine scheme are attached to ideals of Γ(Y, ⊤), by AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine, so the statement may be reduced to that presentation.

public theorem isKernelCokernelAnnihilatedByPower_iff_affine {Y : Scheme.{u}} [IsAffine Y]
    [IsNoetherianRing Γ(Y, ⊤)] (ℐ 𝒦 : Y.IdealSheafData)
    {F G : Stacks.Coherent.CoherentAdicSystems ℐ} (f : F ⟶ G) :
    IsKernelCokernelAnnihilatedByPower 𝒦 f.hom ↔
      IsAffineKernelCokernelAnnihilated (𝒦.ideal ⟨⊤, isAffineOpen_top Y⟩) f

Stacks.Algebraization.isKernelCokernelAnnihilatedByPower_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AnnihilatedLocal.lean, line 202. The attribute's comment: “the equivalence of (1), (2) and (3)”.

Stacks Project, Tag 0888. For a morphism α of Coh(X, 𝓘) on a Noetherian scheme X and a quasi-coherent sheaf of ideals 𝓚, the following are equivalent:

1. one positive power of 𝓚 annihilates every levelwise kernel Ker(α_n) and every levelwise cokernel Coker(α_n);
2. for every affine open U ⊆ X one positive power of 𝓚(U) annihilates Ker(α_U) and Coker(α_U), where α_U is the map of finite modules over the completion attached to α|_U by Tag 087W;
3. the conclusion of (2) holds for the members of some finite affine open covering of X.

A morphism satisfying these conditions is the source's map whose kernel and cokernel are annihilated by a power of 𝓚.

public theorem isKernelCokernelAnnihilatedByPower_tfae {X : Scheme.{u}} [IsNoetherian X]
    (ℐ 𝒦 : X.IdealSheafData) {F G : Stacks.Coherent.CoherentAdicSystems ℐ} (α : F ⟶ G) :
    List.TFAE
      [IsKernelCokernelAnnihilatedByPower 𝒦 α.hom,
        ∀ U : X.affineOpens, IsAffineLocalKernelCokernelAnnihilated 𝒦 α U,
        ∃ (J : Type u) (_ : Finite J) (U : J → X.affineOpens),
          iSup (fun j => (U j).1) = ⊤ ∧
            ∀ j, IsAffineLocalKernelCokernelAnnihilated 𝒦 α (U j)]

Stacks.Algebraization.IsKernelCokernelAnnihilatedByPower, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/PowerAnnihilated.lean, line 435. The attribute's comment: “the notion named by the remark”.

Tag 0888 (1). A morphism α of inverse systems of sheaves of modules has kernel and cokernel annihilated by a power of K if there is one positive exponent t for which K ^ t annihilates both Ker(α_k) and Coker(α_k), simultaneously for every index k.

Kernel and cokernel are taken levelwise, in the abelian category X.Modules. This is the notion the source names at the end of the remark, once its three conditions have been shown equivalent.

public def IsKernelCokernelAnnihilatedByPower (K : X.IdealSheafData) {F G : ℕᵒᵖ ⥤ X.Modules}
    (α : F ⟶ G) : Prop

Tag 088A, a lemma

Tag 088A in the Stacks Project.

Stacks.Coherent.isCoherentAdicSystem_liftedQuotientTower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CoherentAdicSystem/LiftedQuotientAdicSystem.lean, line 286. The attribute's comment: “proof step 4, adic form: the tower of algebraizations lies in Coh(X, 𝒦)”.

Tag 088A: the tower of algebraizations is a coherent adic system along 𝒦. Let X be Noetherian, let ℐ, 𝒦 be quasi-coherent ideal sheaves satisfying hypothesis (1) of [Stacks, Tag 088A] at every level, and let (G_e) be a tower of coherent 𝒪_X-modules, the term e annihilated by 𝒦 ᵉ⁺¹, whose termwise ℐ-completion is identified naturally with the tower of 𝒦 ᵉ⁺¹-reductions of an object (F_n) of Coh(X, ℐ). Then the underlying inverse system of (G_e) is an object of Coh(X, 𝒦).

Only the quotient clause needs proof. The transition G_{e+1} ⟶ G_e descends through the projection onto G_{e+1} / 𝒦 ᵉ⁺¹ G_{e+1}, and Stacks.Coherent.completion_quotientDesc_eq identifies the completion of that descent with the composite of Stacks.Coherent.idealPowerQuotientAdicCompletionIso, the given identification and Stacks.Coherent.idealPowerQuotientAdicCollapseIso, hence with an isomorphism. Both modules are annihilated by 𝒦 ᵉ⁺¹, so completion reflects the isomorphism by Stacks.Coherent.isIso_of_isIso_completion_map_of_power_annihilated.

public theorem isCoherentAdicSystem_liftedQuotientTower [IsNoetherian X]
    (F : CoherentAdicSystems I) (h : IsCompletionEquivalenceOnPowerThickenings I K)
    (G : ℕᵒᵖ ⥤ AlgebraicGeometry.SheafOfModules.CoherentModules X.ringCatSheaf)
    (hG : ∀ e : ℕ, idealPowerMultiple K (e + 1) (G.obj (op e)).obj = ⊥)
    (c : G ⋙ completionFunctor X I ≅
      idealPowerQuotientAdicTower I K ⋙ (evaluation _ _).obj F) :
    IsCoherentAdicSystem K (G ⋙ ObjectProperty.ι _)

Stacks.Coherent.isCoherentAdicSystem_and_annihilated_idealPowerQuotientSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/GrothendieckExistenceII.lean, line 225. The attribute's comment: “proof step 1: the 𝒦ᵉ-reduction is in Coh(X, ℐ), annihilated by 𝒦ᵉ”.

Tag 088A, the opening step of the proof. For a locally Noetherian X, quasi-coherent ideal sheaves ℐ, 𝒦, an exponent e and a coherent adic system (F_n) along ℐ, the reduction n ↦ F_n / 𝒦 ᵉ F_n is again a coherent adic system along ℐ, and every one of its terms is annihilated by 𝒦 ᵉ.

This is the sense in which the source's (F_n / 𝒦 ᵉ F_n) is "a system of Coh(X, ℐ)" lying in the full subcategory of objects annihilated by 𝒦 ᵉ — the subcategory which hypothesis (1) of Tag 088A, read through the closed-immersion equivalence of Tag 087T, identifies with Coh(X_e, ℐ_e).

The first clause is Stacks.Coherent.isCoherentAdicSystem_idealPowerQuotientSystem, whose substance is that the two orders of division agree. The second is Stacks.Algebraization.idealPowerMultiple_idealPowerQuotient_eq_bot, applied to each term; it needs the term to be quasi-coherent, which is the coherence clause of the given system.

public theorem isCoherentAdicSystem_and_annihilated_idealPowerQuotientSystem
    [IsLocallyNoetherian X] {I : X.IdealSheafData} (K : X.IdealSheafData) (e : ℕ)
    {F : ℕᵒᵖ ⥤ X.Modules} (hF : IsCoherentAdicSystem I F) :
    IsCoherentAdicSystem I (idealPowerQuotientSystem K e F) ∧
      ∀ n : ℕ, idealPowerMultiple K e ((idealPowerQuotientSystem K e F).obj (op n)) = ⊥

Stacks.Coherent.isKernelCokernelAnnihilatedByPower_whiskerRight_idealPowerQuotientFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/GrothendieckExistenceII.lean, line 250. The attribute's comment: “proof step 2: the 𝒦ᵉ-reduction of a map with 𝒦ᵗ-annihilated kernel and cokernel has 𝒦²ᵗ-annihilated kernel and cokernel”.

Tag 088A, the second step of the proof. Reducing a morphism of inverse systems of quasi-coherent modules modulo the fixed power 𝒦 ᵉ doubles the exponent in hypothesis (2): if 𝒦 ᵗ annihilates every levelwise kernel and cokernel of α, then 𝒦 ²ᵗ annihilates every levelwise kernel and cokernel of n ↦ (F_n / 𝒦 ᵉ F_n ⟶ G_n / 𝒦 ᵉ G_n).

This is the source's first application of the remark of Tag 0888, which this library has over sheaves of modules as Stacks.Algebraization.idealPowerMultiple_kernel_cokernel_idealPowerQuotientMap; the source applies it a second time further on and reaches 𝒦 ⁴ᵗ.

Applied with (G_n) = H ^∧ it is the statement that the comparison map of hypothesis (2) of Tag 088A survives the reduction of the opening step with its kernel–cokernel condition intact, which is what makes the reduced system an object to which Tag 0889 can be applied.

public theorem isKernelCokernelAnnihilatedByPower_whiskerRight_idealPowerQuotientFunctor
    (K : X.IdealSheafData) (e : ℕ) {F G : ℕᵒᵖ ⥤ X.Modules}
    (hF : ∀ n : ℕ, (F.obj (op n)).IsQuasicoherent)
    (hG : ∀ n : ℕ, (G.obj (op n)).IsQuasicoherent)
    {α : F ⟶ G} (hα : IsKernelCokernelAnnihilatedByPower K α) :
    IsKernelCokernelAnnihilatedByPower K
      (Functor.whiskerRight α (idealPowerQuotientFunctor K e))

Stacks.Coherent.exists_coherent_annihilated_completion_iso_idealPowerQuotientSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/GrothendieckExistenceII.lean, line 315. The attribute's comment: “proof step 3: hypothesis (1) algebraizes the 𝒦ᵉ-reduction”.

Tag 088A, the third step of the proof. Let X be a Noetherian scheme, let ℐ, 𝒦 be quasi-coherent ideal sheaves, let e be an exponent and let (F_n) be an object of Coh(X, ℐ). If hypothesis (1) of Tag 088A holds at the level e — that is, the completion functor of X_e = V(𝒦 ᵉ⁺¹) along ℐ 𝒪_{X_e} is an equivalence — then the 𝒦 ᵉ⁺¹-reduction of (F_n) is the completion of a coherent 𝒪_X-module annihilated by 𝒦 ᵉ⁺¹.

This is where hypothesis (1) enters. The reduction is carried to X_e by the pullback functor of Tag 0887, where the hypothesis algebraizes it to a coherent module M; the algebraization on X is G = i_* M, coherent by Tag 087T and annihilated by 𝒦 ᵉ⁺¹ because it is a direct image along the inclusion of V(𝒦 ᵉ⁺¹). The comparison of completions is Stacks.Coherent.completionPushforwardIso, which identifies the completion of i_* M with the direct image of the completion of M, followed by Stacks.Coherent.idealPowerQuotientSystemPushforwardIso, which is Tag 0EL1 identifying i_* i^* F_n with F_n / 𝒦 ᵉ⁺¹ F_n.

public theorem exists_coherent_annihilated_completion_iso_idealPowerQuotientSystem
    [IsNoetherian X] (I K : X.IdealSheafData) (e : ℕ) (Fsys : CoherentAdicSystems I)
    (h : letI : IsLocallyNoetherian (K ^ (e + 1)).subscheme :=
        LocallyOfFiniteType.isLocallyNoetherian (K ^ (e + 1)).subschemeι
      (completionFunctor (K ^ (e + 1)).subscheme
        (I.comap (K ^ (e + 1)).subschemeι)).IsEquivalence) :
    ∃ G : AlgebraicGeometry.SheafOfModules.CoherentModules X.ringCatSheaf,
      idealPowerMultiple K (e + 1) G.obj = ⊥ ∧
      Nonempty (((completionFunctor X I).obj G).obj ≅
        idealPowerQuotientSystem K (e + 1) Fsys.obj)

Stacks.Coherent.exists_coherentAdicSystem_completion_iso_idealPowerQuotientSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/GrothendieckExistenceII.lean, line 374. The attribute's comment: “proof step 4: the algebraizations G_e assemble into an object of Coh(X, 𝒦)”.

Tag 088A, the fourth step of the proof: the algebraizations assemble. Let X be a Noetherian scheme, let ℐ, 𝒦 be quasi-coherent ideal sheaves and let (F_n) be an object of Coh(X, ℐ). If hypothesis (1) of Tag 088A holds at every level — the completion functor of X_e = V(𝒦 ᵉ⁺¹) along ℐ 𝒪_{X_e} is an equivalence — then the coherent modules G_e algebraizing the reductions (F_n / 𝒦 ᵉ⁺¹ F_n) form an object of Coh(X, 𝒦).

The modules themselves and their defining property are the third step, Stacks.Coherent.exists_coherent_annihilated_completion_iso_idealPowerQuotientSystem. What is added here is the identification G_{e+1} / 𝒦 ᵉ⁺¹ G_{e+1} ≅ G_e, read off the completions by Stacks.Coherent.nonempty_idealPowerQuotient_iso_of_completion_iso: completion along ℐ carries the left-hand side to

(F_n / 𝒦 ᵉ⁺² F_n) / 𝒦 ᵉ⁺¹ (…) ≅ F_n / 𝒦 ᵉ⁺¹ F_n,

by Stacks.Coherent.completionIdealPowerQuotientSystemIso and Stacks.Coherent.idealPowerQuotientSystemCollapseIso, which is the completion of the right-hand side; and completion along ℐ, although not known to be full on all of Coh(𝒪_X), is fully faithful on the modules annihilated by 𝒦 ᵉ⁺¹. The assembly of the identified modules into an object of Coh(X, 𝒦) is Stacks.Coherent.exists_coherentAdicSystem_of_succQuotientIso.

The conclusion keeps the sequence G alongside the assembled system, because the rest of the source's argument speaks about the terms: the comparison with H ^∧ is built level by level.

public theorem exists_coherentAdicSystem_completion_iso_idealPowerQuotientSystem
    [IsNoetherian X] (I K : X.IdealSheafData) (Fsys : CoherentAdicSystems I)
    (h : ∀ e : ℕ,
      letI : IsLocallyNoetherian (K ^ (e + 1)).subscheme :=
        LocallyOfFiniteType.isLocallyNoetherian (K ^ (e + 1)).subschemeι
      (completionFunctor (K ^ (e + 1)).subscheme
        (I.comap (K ^ (e + 1)).subschemeι)).IsEquivalence) :
    ∃ Gsys : CoherentAdicSystems K,
      ∃ G : ℕ → AlgebraicGeometry.SheafOfModules.CoherentModules X.ringCatSheaf,
        (∀ e : ℕ, Gsys.obj.obj (op e) = (G e).obj) ∧
        ∀ e : ℕ, idealPowerMultiple K (e + 1) (G e).obj = ⊥ ∧
          Nonempty (((completionFunctor X I).obj (G e)).obj ≅
            idealPowerQuotientSystem K (e + 1) Fsys.obj)

Stacks.Coherent.exists_lifted_quotient_tower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/GrothendieckExistenceII.lean, line 423. The attribute's comment: “proof step 4, natural form: the algebraizations G_e form a tower whose ℐ-completion is the tower of 𝒦-power reductions of (F_n)”.

Tag 088A, the fourth step in the form the rest of the proof needs it. Under hypothesis (1) of Tag 088A at every level, the algebraizations G_e of the reductions (F_n / 𝒦 ᵉ⁺¹ F_n) form a tower of coherent 𝒪_X-modules, the term e annihilated by 𝒦 ᵉ⁺¹, whose termwise ℐ-completion is identified with the tower of reductions naturally in e.

Stacks.Coherent.exists_coherentAdicSystem_completion_iso_idealPowerQuotientSystem assembles the same modules into an object of Coh(X, 𝒦), but its identification of completions is one isomorphism for each e separately. What is added here is the naturality: the transition G_{e+1} ⟶ G_e is obtained by lifting the transition of the tower of reductions through the full faithfulness of completion on the 𝒦 ᵉ⁺²-annihilated modules (Stacks.Coherent.exists_unique_completion_preimage_of_power_annihilated), so the chosen isomorphisms commute with the transitions by construction.

This is the datum that Stacks.Coherent.exists_tower_map_to_completion consumes to produce the comparison (G_e) ⟶ H ^∧_𝒦 along 𝒦.

public theorem exists_lifted_quotient_tower [IsNoetherian X] (I K : X.IdealSheafData)
    (Fsys : CoherentAdicSystems I)
    (h : ∀ e : ℕ,
      letI : IsLocallyNoetherian (K ^ (e + 1)).subscheme :=
        LocallyOfFiniteType.isLocallyNoetherian (K ^ (e + 1)).subschemeι
      (completionFunctor (K ^ (e + 1)).subscheme
        (I.comap (K ^ (e + 1)).subschemeι)).IsEquivalence) :
    ∃ G : ℕᵒᵖ ⥤ AlgebraicGeometry.SheafOfModules.CoherentModules X.ringCatSheaf,
      (∀ e : ℕ, idealPowerMultiple K (e + 1) (G.obj (op e)).obj = ⊥) ∧
      Nonempty (G ⋙ completionFunctor X I ≅
        idealPowerQuotientAdicTower I K ⋙ (evaluation _ _).obj Fsys)

Stacks.Coherent.exists_lifted_quotient_tower_comparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/GrothendieckExistenceII.lean, line 490. The attribute's comment: “proof step 5: the comparison (G_e) ⟶ H^∧_𝒦 along 𝒦, with its levelwise kernels and cokernels annihilated by a power of 𝒦”.

Tag 088A, the fifth step: the comparison along 𝒦 exists and satisfies the hypothesis of Tag 0889. Let X be Noetherian, let ℐ, 𝒦 be quasi-coherent ideal sheaves satisfying hypothesis (1) of Tag 088A at every level, and let α : (F_n) ⟶ H ^∧_ℐ be a comparison whose levelwise kernels and cokernels are annihilated by a power of 𝒦 — hypothesis (2). Then the tower (G_e) of algebraizations of the reductions carries a morphism γ : (G_e) ⟶ H ^∧_𝒦 whose kernels and cokernels are annihilated by a single positive power of 𝒦.

This is the whole of the source's passage from the comparison along ℐ to the comparison along 𝒦: the tower is Stacks.Coherent.exists_lifted_quotient_tower, the comparison is Stacks.Coherent.exists_tower_map_to_completion — the reduction of α lifted through the fullness of completion on 𝒦-power-annihilated towers — and the annihilation is Stacks.Coherent.idealPowerMultiple_kernel_cokernel_tower_map_eq_bot, the remark of Tag 0888 followed by the reflection of annihilation along completion.

What remains of the proof of Tag 088A after this is the final identification: Tag 0889 applied to γ algebraizes it, and its uniqueness clause, threaded through the two towers, identifies (F_n) with the completion of the resulting module.

public theorem exists_lifted_quotient_tower_comparison [IsNoetherian X]
    (I K : X.IdealSheafData) (Fsys : CoherentAdicSystems I)
    (h : ∀ e : ℕ,
      letI : IsLocallyNoetherian (K ^ (e + 1)).subscheme :=
        LocallyOfFiniteType.isLocallyNoetherian (K ^ (e + 1)).subschemeι
      (completionFunctor (K ^ (e + 1)).subscheme
        (I.comap (K ^ (e + 1)).subschemeι)).IsEquivalence)
    (H : AlgebraicGeometry.SheafOfModules.CoherentModules X.ringCatSheaf)
    (α : Fsys ⟶ (completionFunctor X I).obj H)
    (hα : IsKernelCokernelAnnihilatedByPower K α.hom) :
    ∃ (G : ℕᵒᵖ ⥤ AlgebraicGeometry.SheafOfModules.CoherentModules X.ringCatSheaf)
      (γ : G ⟶ completionTermTower K H),
      (∀ e : ℕ, idealPowerMultiple K (e + 1) (G.obj (op e)).obj = ⊥) ∧
      Nonempty (G ⋙ completionFunctor X I ≅
        idealPowerQuotientAdicTower I K ⋙ (evaluation _ _).obj Fsys) ∧
      ∃ s : ℕ, 0 < s ∧ ∀ e : ℕ,
        idealPowerMultiple K s (kernel (C := X.Modules) (γ.app (op e)).hom) = ⊥ ∧
          idealPowerMultiple K s (cokernel (C := X.Modules) (γ.app (op e)).hom) = ⊥

Stacks.Coherent.essImage_completionFunctor_of_pow_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/GrothendieckExistenceII.lean, line 534. The attribute's comment: “the case ℐᵐ ≤ 𝒦, hypothesis (1) unused; incomparable case not claimed”.

Tag 088A in the case ℐ ᵐ ≤ 𝒦. Let X be a Noetherian scheme, let ℐ, 𝒦 be quasi-coherent ideal sheaves on X with ℐ ᵐ ≤ 𝒦 for some m ≥ 1, let H be a coherent 𝒪_X-module and let (F_n) be an object of Coh(X, ℐ) admitting a map α : (F_n) ⟶ H ^∧ whose levelwise kernels and cokernels are annihilated by a power of 𝒦. Then (F_n) is in the essential image of the completion functor of Tag 0880.

Hypothesis (1) of the source is not needed here, and no reduction modulo a power of 𝒦 occurs: the containment turns hypothesis (2) into the hypothesis of Tag 0889 part (1) by Stacks.Coherent.isKernelCokernelAnnihilatedByPower_of_pow_le, and Stacks.Algebraization.exists_unique_algebraization_of_isNoetherian then algebraizes α, delivering a coherent module F and an isomorphism (F_n) ≅ F ^∧. The isomorphism is of the underlying inverse systems and is promoted to the full subcategory Coh(X, ℐ) by CategoryTheory.ObjectProperty.isoMk.

The source's own application has ℐ the pullback of an ideal of the base and 𝒦 the ideal of the complement of the dense open on which Chow's lemma is an isomorphism; no power of ℐ is contained in 𝒦 there, so this case does not cover it.

public theorem essImage_completionFunctor_of_pow_le [IsNoetherian X] {I K : X.IdealSheafData}
    {m : ℕ} (hm : 0 < m) (hIK : I ^ m ≤ K)
    (H : AlgebraicGeometry.SheafOfModules.CoherentModules X.ringCatSheaf)
    (Fsys : CoherentAdicSystems I)
    (α : Fsys.obj ⟶ ((completionFunctor X I).obj H).obj)
    (hα : IsKernelCokernelAnnihilatedByPower K α) :
    (completionFunctor X I).essImage Fsys

Stacks.Coherent.essImage_completionFunctor_of_isKernelCokernelAnnihilatedByPower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/GrothendieckExistenceII.lean, line 580.

[Stacks, Tag 088A]. Let X be a Noetherian scheme and let ℐ, 𝒦 ⊆ 𝒪_X be quasi-coherent ideal sheaves. Let (F_n) be an object of Coh(X, ℐ) and suppose

1. for every e, completion along ℐ 𝒪_{X_e} is an equivalence on Coh(𝒪_{X_e}), where X_e = V(𝒦 ᵉ⁺¹) is the closed subscheme cut out by the positive power 𝒦 ᵉ⁺¹, and
2. there is a coherent 𝒪_X-module H and a morphism α : (F_n) ⟶ H ^∧_ℐ whose levelwise kernels and cokernels are annihilated by a power of 𝒦.

Then (F_n) is in the essential image of the completion functor of [Stacks, Tag 0880]: it is the ℐ-completion of a coherent 𝒪_X-module.

The proof is the source's, assembled from the steps carried above and in FormalGeometry.CoherentAdicSystem. Dividing (F_n) by the powers of 𝒦 and algebraizing the reductions with hypothesis (1) produces the tower (G_e) of Stacks.Coherent.exists_lifted_quotient_tower, which is an object of Coh(X, 𝒦) by Stacks.Coherent.isCoherentAdicSystem_liftedQuotientTower; the reduction of α, lifted through the fullness of completion on the annihilated towers, is the comparison γ : (G_e) ⟶ H ^∧_𝒦 of Stacks.Coherent.exists_tower_map_to_completion, and its levelwise kernels and cokernels are annihilated by one power of 𝒦 (Stacks.Coherent.idealPowerMultiple_kernel_cokernel_tower_map_eq_bot). So [Stacks, Tag 0889] part (1) algebraizes γ to a coherent module M with (G_e) ≅ M ^∧_𝒦.

What remains is to recognize (F_n) as M ^∧_ℐ. Reading the identification of the completed tower (G_e) ^∧_ℐ with the tower of reductions of (F_n) along the other index (Stacks.Coherent.liftedQuotientRowTowerIso) turns the algebraization of γ into an identification of the 𝒦-completions of the terms of (F_n) and of M ^∧_ℐ, compatible with α and with α ^∧ by Stacks.Coherent.liftedQuotientRowIso_map_to_completion; the uniqueness clause of Tag 0889 applied termwise then identifies the two systems, which is Stacks.Coherent.nonempty_iso_of_completion_iso_over_power_annihilated.

Stacks.Coherent.essImage_completionFunctor_of_pow_le is the special case ℐ ᵐ ≤ 𝒦, where hypothesis (1) is not needed.

public theorem essImage_completionFunctor_of_isKernelCokernelAnnihilatedByPower [IsNoetherian X]
    (I K : X.IdealSheafData) (Fsys : CoherentAdicSystems I)
    (h : ∀ e : ℕ,
      letI : IsLocallyNoetherian (K ^ (e + 1)).subscheme :=
        LocallyOfFiniteType.isLocallyNoetherian (K ^ (e + 1)).subschemeι
      (completionFunctor (K ^ (e + 1)).subscheme
        (I.comap (K ^ (e + 1)).subschemeι)).IsEquivalence)
    (H : AlgebraicGeometry.SheafOfModules.CoherentModules X.ringCatSheaf)
    (α : Fsys ⟶ (completionFunctor X I).obj H)
    (hα : IsKernelCokernelAnnihilatedByPower K α.hom) :
    (completionFunctor X I).essImage Fsys

Tag 088B, a lemma

Tag 088B in the Stacks Project.

Stacks.Coherent.exists_isKernelCokernelAnnihilatedByPower_comparisonMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionProper/ExceptionalComparisonMap.lean, line 75.

Stacks 088B. Let Y be a Noetherian scheme and let 𝒥, 𝒦 ⊆ 𝒪_Y be quasi-coherent sheaves of ideals. Let f : X ⟶ Y be a proper morphism which is an isomorphism over V = Y ∖ V(𝒦), and set ℐ = f^{-1}𝒥 𝒪_X. Let (𝒢_n) be an object of Coh(Y, 𝒥), let 𝓕 be a coherent 𝒪_X-module, and let β : (f^*𝒢_n) ⟶ 𝓕^ be an isomorphism in Coh(X, ℐ). Then there exists a map

α : (𝒢_n) ⟶ (f_*𝓕)^

in Coh(Y, 𝒥) whose kernel and cokernel are annihilated by a power of 𝒦.

public theorem exists_isKernelCokernelAnnihilatedByPower_comparisonMap
    {X Y : Scheme.{u}} [IsNoetherian Y] (J K : Y.IdealSheafData)
    (f : X ⟶ Y) [IsProper f] (hf : IsIso (f ∣_ K.support.compl))
    (G : CoherentAdicSystems J) (F : X.Modules) [F.IsCoherent] :
    letI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian f
    letI : IsNoetherian X :=
      { toIsLocallyNoetherian := LocallyOfFiniteType.isLocallyNoetherian f
        toCompactSpace := QuasiCompact.compactSpace_of_compactSpace f }
    letI : ((Scheme.Modules.pushforward f).obj F).IsCoherent :=
      AlgebraicGeometry.ProperCoherenceWitness.isCoherent_pushforward f F
    ∀ _β : (coherentAdicPullback f J).obj G ≅
        (completionFunctor X (J.comap f)).obj ⟨F, inferInstance⟩,
      ∃ α : G ⟶ (completionFunctor Y J).obj
          ⟨(Scheme.Modules.pushforward f).obj F, inferInstance⟩,
        IsKernelCokernelAnnihilatedByPower K α.hom

Tag 088C, a proposition

Tag 088C in the Stacks Project.

Stacks.Algebraization.isEquivalence_completionFunctor_of_devissage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionProper/Devissage.lean, line 267. The attribute's comment: “for a proper f, with the theorem on formal functions in degree zero (087U) as the hypothesis hFF and the inductive step of the source's Noetherian induction over the quasi-coherent ideal sheaves of X as the hypothesis hDev -- that a coherent adic system killed by an ideal sheaf K is in the essential image of the completion functor as soon as every coherent adic system killed by a strictly larger ideal sheaf is. The induction itself, its ascending chain condition (for which the source cites 01Y8) and its conclusion at the zero ideal sheaf are proved unconditionally here; the source supplies hDev from Chow's lemma (0200), 087T, the projective case (0885), the coherence of a proper direct image (02O5) and 088A with 088B”.

Stacks 088C. Let A be a Noetherian ring complete with respect to an ideal I, let f : X ⟶ Spec A be a proper morphism of schemes and set 𝓘 = I · 𝒪_X. Then the completion functor Coh(𝒪_X) ⥤ Coh(X, 𝓘) of Stacks 0880 is an equivalence — faithful, full and essentially surjective — granted

• hFF, the theorem on formal functions in degree zero (Stacks 087U), which is what Stacks 0883 assumes for full faithfulness and which this library does not carry unconditionally, and
• hDev, the inductive step of the source's Noetherian induction: a coherent 𝓘-adic system killed by a quasi-coherent ideal sheaf K is in the essential image of the completion functor as soon as every coherent 𝓘-adic system killed by an ideal sheaf strictly larger than K is.

Everything else is proved here. Full faithfulness is Stacks 0883 read through hFF. Essential surjectivity is the Noetherian induction essImage_completionFunctor_of_devissage applied at the zero ideal sheaf, which kills every system by isSystemAnnihilatedBy_bot; the induction is legitimate because the quasi-coherent ideal sheaves of the Noetherian scheme X satisfy the ascending chain condition. Noetherianity of X is not an added hypothesis: local Noetherianity follows from LocallyOfFiniteType f over the Noetherian base and quasi-compactness from the universal closedness of f and the quasi-compactness of Spec A.

hDev is the source's own step. Granted hFF it is, like the generation hypothesis hGen of Stacks.Algebraization.isEquivalence_completionFunctor_of_exists_epi, equivalent to the conclusion; what differs is the obligation. hGen grants nothing and is not a step of the source's proof for a proper morphism — the source proves it only in the projective case, by Stacks 0884 — whereas hDev is discharged one ideal sheaf at a time with the statement already available on every strictly larger ideal sheaf. The source supplies hDev by Chow's lemma (Stacks 0200), Stacks 087T, the projective case Stacks 0885, the coherence of a proper direct image (Stacks 02O5) and Stacks 088A together with 088B; of those this library carries 0200 and 087T unconditionally, has 0885 only with hFF and a generation hypothesis resting on the absent Stacks 0884 and 0897, and carries none of 02O5, 088A, 088B.

public theorem isEquivalence_completionFunctor_of_devissage
    (A : Type u) [CommRing A] [IsNoetherianRing A] (I : Ideal A) [IsAdicComplete I A]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of A)) [IsProper f]
    (hFF : letI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian f
      ∀ H : AlgebraicGeometry.SheafOfModules.CoherentModules X.ringCatSheaf,
        IsIso (globalSectionsToLimit (baseIdealSheaf A I f) H))
    (hDev : letI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian f
      ∀ K : X.IdealSheafData,
        (∀ K' : X.IdealSheafData, K < K' →
            ∀ 𝓖 : Stacks.Coherent.CoherentAdicSystems (baseIdealSheaf A I f),
              IsSystemAnnihilatedBy K' 𝓖.obj →
                (completionFunctor X (baseIdealSheaf A I f)).essImage 𝓖) →
          ∀ 𝓕 : Stacks.Coherent.CoherentAdicSystems (baseIdealSheaf A I f),
            IsSystemAnnihilatedBy K 𝓕.obj →
              (completionFunctor X (baseIdealSheaf A I f)).essImage 𝓕) :
    letI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian f
    (completionFunctor X (baseIdealSheaf A I f)).IsEquivalence

Stacks.Algebraization.isEquivalence_completionFunctor_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionProper/GrothendieckExistenceProper.lean, line 136.

Stacks 088C: Grothendieck's existence theorem for a proper morphism. Let A be a Noetherian ring complete with respect to an ideal I, let f : X ⟶ Spec A be a proper morphism of schemes and set 𝓘 = I · 𝒪_X. Then the completion functor Coh(𝒪_X) ⥤ Coh(X, 𝓘) of Stacks 0880 is an equivalence.

This is Stacks.Algebraization.isEquivalence_completionFunctor_of_devissage with both of its hypotheses discharged: hFF by the theorem on formal functions in degree zero over a complete base, isIso_globalSectionsToLimit_of_isProper, and hDev by Stacks.Coherent.essImage_completionFunctor_of_devissageStep.

public theorem isEquivalence_completionFunctor_of_isProper
    (A : Type u) [CommRing A] [IsNoetherianRing A] (I : Ideal A) [IsAdicComplete I A]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of A)) [IsProper f] :
    letI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian f
    (completionFunctor X (baseIdealSheaf A I f)).IsEquivalence

Sources

• Section 30.25, Tag 0886
• AxiomMath/Stacks at 5ed82d14

LeanIdeal.existsUnique_canonicalMap_of_smul_eq_bot · Ideal.pow_le_annihilator_ker_mapQ_of_exact · Ideal.pow_le_annihilator_coker_mapQ_of_exact · Stacks.Algebraization.idealPowerMultiple_kernel_cokernel_idealPowerQuotientMap · Stacks.Algebraization.isKernelCokernelAnnihilatedByPower_iff_affine · Stacks.Algebraization.isKernelCokernelAnnihilatedByPower_tfae · Stacks.Algebraization.IsKernelCokernelAnnihilatedByPower · Stacks.Coherent.isCoherentAdicSystem_liftedQuotientTower

Section30.26 Being proper over a base#

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

Tag 0CYL, a lemma

Tag 0CYL in the Stacks Project.

AlgebraicGeometry.isProperOver_iff_exists_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Proper/ProperClosedSubset.lean, line 136. The attribute's comment: “parts (1) and (2)”. References: EGA II (5.4.10), “indep. of subscheme”.

Stacks 0CYL, parts (1) and (2). The reduced closed subscheme on Z is proper over S exactly when some closed subscheme structure on Z is proper over S.

public theorem isProperOver_iff_exists_isProper :
    IsProperOver f Z ↔ ∃ I : X.IdealSheafData, I.support = Z ∧ IsProper (I.subschemeι ≫ f)

AlgebraicGeometry.exists_isProper_iff_forall_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Proper/ProperClosedSubset.lean, line 148. The attribute's comment: “parts (2) and (3)”. References: EGA II (5.4.10), “indep. of subscheme”.

Stacks 0CYL, parts (2) and (3). If one closed subscheme structure on Z is proper over S, then every closed subscheme structure on Z is proper over S.

public theorem exists_isProper_iff_forall_isProper :
    (∃ I : X.IdealSheafData, I.support = Z ∧ IsProper (I.subschemeι ≫ f)) ↔
      ∀ I : X.IdealSheafData, I.support = Z → IsProper (I.subschemeι ≫ f)

Tag 0CYM, a definition

Tag 0CYM in the Stacks Project.

AlgebraicGeometry.IsProperOver, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Proper/ProperClosedSubset.lean, line 82.

Stacks 0CYM. A closed subset Z of X is proper over S if its reduced induced closed subscheme is proper over S.

public abbrev IsProperOver {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    (Z : Closeds X) : Prop

Tag 0CYN, a lemma

Tag 0CYN in the Stacks Project.

AlgebraicGeometry.isProperOver_of_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Proper/ProperClosedSubset.lean, line 159.

Stacks 0CYN. A closed subset of a closed subset proper over the base is proper over the base.

public theorem isProperOver_of_le {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    {Y Z : Closeds X} (hYZ : Y ≤ Z) (hZ : IsProperOver f Z) : IsProperOver f Y

Tag 0CYP, a lemma

Tag 0CYP in the Stacks Project.

AlgebraicGeometry.isProperOver_preimage_baseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Proper/ProperClosedSubset.lean, line 168.

Stacks 0CYP. A closed subset proper over the base remains proper after base change.

public theorem isProperOver_preimage_baseChange {X' X S' S : Scheme.{u}}
    (g' : X' ⟶ X) (f' : X' ⟶ S') (f : X ⟶ S) (g : S' ⟶ S)
    (h : IsPullback g' f' f g) [LocallyOfFiniteType f]
    (Z : Closeds X) (hZ : IsProperOver f Z) :
    haveI : LocallyOfFiniteType f' := MorphismProperty.of_isPullback h inferInstance
    IsProperOver f' (Z.preimage g'.continuous)

Tag 0CYQ, a lemma

Tag 0CYQ in the Stacks Project.

AlgebraicGeometry.isClosed_image_of_isProperOver, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/ProperOverBase/Functoriality.lean, line 74. The attribute's comment: “image_separated”. References: SGA 4 XVII (6.1.1), “Clause (i)”.

The image of a closed subset proper over the base is closed in a separated scheme locally of finite type over that base.

lemma isClosed_image_of_isProperOver {X Y S : Scheme.{u}}
    (p : X ⟶ S) (g : Y ⟶ S) (f : X ⟶ Y) (hfg : f ≫ g = p)
    [LocallyOfFiniteType p] [LocallyOfFiniteType g] [IsSeparated g]
    (Z : Closeds X) (hZ : IsProperOver p Z) :
    IsClosed (f.base '' (Z : Set X))

AlgebraicGeometry.isProperOver_image, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/ProperOverBase/Functoriality.lean, line 87. The attribute's comment: “image_separated”. References: EGA II (5.4.10), “more general”.

The image of a closed subset proper over the base is itself proper over the base, when the target is separated and locally of finite type.

lemma isProperOver_image {X Y S : Scheme.{u}}
    (p : X ⟶ S) (g : Y ⟶ S) (f : X ⟶ Y) (hfg : f ≫ g = p)
    [LocallyOfFiniteType p] [LocallyOfFiniteType g] [IsSeparated g]
    (Z : Closeds X) (hZ : IsProperOver p Z) :
    IsProperOver g
      ⟨f.base '' (Z : Set X), isClosed_image_of_isProperOver p g f hfg Z hZ⟩

AlgebraicGeometry.isProperOver_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/ProperOverBase/Functoriality.lean, line 106. The attribute's comment: “preimage_proper”.

The inverse image of a closed subset proper over the base along a proper morphism is proper over the base.

theorem isProperOver_preimage {X Y S : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ S)
    [IsProper f] [LocallyOfFiniteType g] (Z : Closeds Y)
    (hZ : IsProperOver g Z) :
    IsProperOver (f ≫ g) (Z.preimage f.continuous)

AlgebraicGeometry.Scheme.Hom.closedImage, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Proper/ProperClosedSubset.lean, line 200. The attribute's comment: “image_universally_closed”.

Stacks 0CYQ. The image of a closed subset under a universally closed morphism, as a closed subset.

public def Scheme.Hom.closedImage {X Y : Scheme.{u}} (f : X ⟶ Y) [UniversallyClosed f]
    (Z : Closeds X) : Closeds Y

AlgebraicGeometry.isProperOver_closedImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Proper/ProperClosedSubset.lean, line 207. The attribute's comment: “image_universally_closed”.

Stacks 0CYQ. The closed image of a closed subset proper over the base is proper over the base.

public theorem isProperOver_closedImage {X Y S : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ S)
    [UniversallyClosed f] [LocallyOfFiniteType (f ≫ g)] [LocallyOfFiniteType g]
    (Z : Closeds X) (hZ : IsProperOver (f ≫ g) Z) :
    IsProperOver g (f.closedImage Z)

Tag 0CYR, a lemma

Tag 0CYR in the Stacks Project.

AlgebraicGeometry.isProperOver_sup, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Proper/ProperClosedSubset.lean, line 261.

Stacks 0CYR. The union of two closed subsets proper over the base is proper over the base.

public theorem isProperOver_sup {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    (Z W : Closeds X) (hZ : IsProperOver f Z) (hW : IsProperOver f W) :
    IsProperOver f (Z ⊔ W)

AlgebraicGeometry.isProperOver_iSup, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Proper/ProperClosedSubset.lean, line 312.

Stacks 0CYR. A finite union of closed subsets proper over the base is proper over the base.

public theorem isProperOver_iSup {X S : Scheme.{u}} (f : X ⟶ S) [LocallyOfFiniteType f]
    {ι : Type v} [Finite ι] (Z : ι → Closeds X) (hZ : ∀ i, IsProperOver f (Z i)) :
    IsProperOver f (iSup Z)

Tag 0CYS, a lemma

Tag 0CYS in the Stacks Project.

AlgebraicGeometry.Scheme.Modules.isProperOver_supp_iff_isProper_schemeTheoreticSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Proper/ProperSupport.lean, line 62. The attribute's comment: “conditions (1) and (2)”.

The support of a quasi-coherent module of finite type is proper over the base if and only if its scheme-theoretic support is proper over the base.

public theorem isProperOver_supp_iff_isProper_schemeTheoreticSupport :
    IsProperOver f ⟨SheafOfModules.supp F, SheafOfModules.isClosed_supp F⟩ ↔
      IsProper ((schemeTheoreticSupport F).subschemeι ≫ f)

AlgebraicGeometry.Scheme.Modules.isProper_schemeTheoreticSupport_iff_exists_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Morphisms/Proper/ProperSupport.lean, line 76. The attribute's comment: “conditions (2) and (3)”.

The scheme-theoretic support of a quasi-coherent module F of finite type is proper over the base if and only if there is a closed subscheme of X proper over the base carrying a quasi-coherent module of finite type whose direct image is F.

public theorem isProper_schemeTheoreticSupport_iff_exists_pushforward :
    IsProper ((schemeTheoreticSupport F).subschemeι ≫ f) ↔
      ∃ (J : X.IdealSheafData) (G : J.subscheme.Modules),
        G.IsFiniteType ∧ G.IsQuasicoherent ∧ IsProper (J.subschemeι ≫ f) ∧
          Nonempty ((Scheme.Modules.pushforward J.subschemeι).obj G ≅ F)

Tag 0CYT, a lemma

Tag 0CYT in the Stacks Project.

AlgebraicGeometry.isProperOver_supp_pullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Perfect/SupportPullback/BaseChange.lean, line 47.

In a cartesian square, base change preserves properness of the support of a finite type module over the base.

theorem isProperOver_supp_pullback {X' X S' S : Scheme.{u}}
    (g' : X' ⟶ X) (f' : X' ⟶ S') (f : X ⟶ S) (g : S' ⟶ S)
    (h : IsPullback g' f' f g) [LocallyOfFiniteType f]
    (F : X.Modules) [F.IsFiniteType]
    (hF : IsProperOver f ⟨SheafOfModules.supp F, SheafOfModules.isClosed_supp F⟩) :
    letI : LocallyOfFiniteType f' := MorphismProperty.of_isPullback h inferInstance
    letI : ((Scheme.Modules.pullback g').obj F).IsFiniteType :=
      SheafOfModules.pullback_isFiniteType g'.toLRSHom.toShHom F
    IsProperOver f'
      ⟨SheafOfModules.supp ((Scheme.Modules.pullback g').obj F),
        SheafOfModules.isClosed_supp _⟩

Tag 0CYU, a lemma

Tag 0CYU in the Stacks Project.

AlgebraicGeometry.isSerreClass_hasProperSupport_coherentModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/ProperOverBase/CoherentSerreClass.lean, line 68. The attribute's comment: “part (2)”.

Stacks Project, Tag 0CYU, part (2). For f : X ⟶ S locally of finite type with S locally Noetherian, the coherent 𝒪_X-modules whose support is proper over S form a Serre subcategory of the abelian category of coherent 𝒪_X-modules.

The zero module has empty support, which is proper over S; and the support of the middle term of an exact sequence of coherent modules is contained in the union of the supports of the outer two, a union of two closed subsets proper over S being proper over S.

theorem isSerreClass_hasProperSupport_coherentModules [IsLocallyNoetherian S] :
    ObjectProperty.IsSerreClass
      (C := SheafOfModules.CoherentModules X.ringCatSheaf)
      (fun F => Stacks.Algebraization.HasProperSupport f F.obj)

AlgebraicGeometry.isProperOver_biprod_support, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/ProperOverBase/ModuleSupport.lean, line 190. The attribute's comment: “sheaf_operations”.

The direct sum of two sheaves with proper support has proper support.

theorem isProperOver_biprod_support {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] (F G : X.Modules)
    (b : BinaryBicone F G) (hb : b.IsBilimit)
    (hF : ∃ Z : Closeds X, ((Z : Set X) = SheafOfModules.supp F ∧
      IsProperOver f Z))
    (hG : ∃ Z : Closeds X, ((Z : Set X) = SheafOfModules.supp G ∧
      IsProperOver f Z)) :
    ∃ Z : Closeds X, ((Z : Set X) = SheafOfModules.supp b.pt ∧
      IsProperOver f Z)

AlgebraicGeometry.isProperOver_extension_support, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/ProperOverBase/ModuleSupport.lean, line 209. The attribute's comment: “sheaf_operations”.

A short exact extension of sheaves with proper support has proper support.

theorem isProperOver_extension_support {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] (E : ShortComplex X.Modules) (hE : E.ShortExact)
    (hF : ∃ Z : Closeds X, ((Z : Set X) = SheafOfModules.supp E.X₁ ∧
      IsProperOver f Z))
    (hG : ∃ Z : Closeds X, ((Z : Set X) = SheafOfModules.supp E.X₃ ∧
      IsProperOver f Z)) :
    ∃ Z : Closeds X, ((Z : Set X) = SheafOfModules.supp E.X₂ ∧
      IsProperOver f Z)

AlgebraicGeometry.isProperOver_image_support, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/ProperOverBase/ModuleSupport.lean, line 222. The attribute's comment: “sheaf_operations”.

The image of a morphism from a finite type sheaf with proper support to an arbitrary sheaf of modules has proper support.

theorem isProperOver_image_support {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] (F G : X.Modules)
    [F.IsFiniteType]
    (u : F ⟶ G)
    (hF : ∃ Z : Closeds X, ((Z : Set X) = SheafOfModules.supp F ∧
      IsProperOver f Z)) :
    ∃ Z : Closeds X, ((Z : Set X) = SheafOfModules.supp (Abelian.image u) ∧
      IsProperOver f Z)

AlgebraicGeometry.isProperOver_cokernel_support, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/ProperOverBase/ModuleSupport.lean, line 236. The attribute's comment: “sheaf_operations”.

The cokernel of a morphism from an arbitrary sheaf of modules to a finite type sheaf with proper support has proper support.

theorem isProperOver_cokernel_support {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] (F G : X.Modules)
    [G.IsFiniteType]
    (u : F ⟶ G)
    (hG : ∃ Z : Closeds X, ((Z : Set X) = SheafOfModules.supp G ∧
      IsProperOver f Z)) :
    ∃ Z : Closeds X, ((Z : Set X) = SheafOfModules.supp (cokernel u) ∧
      IsProperOver f Z)

AlgebraicGeometry.isProperOver_quotient_support, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Cohomology/ProperOverBase/ModuleSupport.lean, line 249. The attribute's comment: “sheaf_operations”.

A quotient of a finite type sheaf with proper support has proper support.

theorem isProperOver_quotient_support {X S : Scheme.{u}} (f : X ⟶ S)
    [LocallyOfFiniteType f] (F Q : X.Modules)
    [F.IsFiniteType]
    (q : F ⟶ Q) [Epi q]
    (hF : ∃ Z : Closeds X, ((Z : Set X) = SheafOfModules.supp F ∧
      IsProperOver f Z)) :
    ∃ Z : Closeds X, ((Z : Set X) = SheafOfModules.supp Q ∧
      IsProperOver f Z)

Tag 08DS, a lemma

Tag 08DS in the Stacks Project.

Stacks.AlgebraicGeometry.ProperSupportCoherent.isCoherent_higherDirectImage_of_properSupp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ProperSupportCoherent/Unconditional.lean, line 60.

Let S be locally Noetherian, let f : X ⟶ S be locally of finite type and let F be a quasi-coherent 𝒪_X-module of finite type whose support is proper over S. Then the higher direct image R ᵖ f_* F is a coherent 𝒪_S-module in every degree.

theorem isCoherent_higherDirectImage_of_properSupp
    (hF : IsProperOver f ⟨SheafOfModules.supp F, SheafOfModules.isClosed_supp F⟩) (p : ℤ) :
    (((Scheme.Modules.pushforward f).rightDerivedPlus p).obj F).IsCoherent

Tag 0CYV, a lemma

Tag 0CYV in the Stacks Project.

Stacks.Coherent.isSerreClass_hasProperSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/ProperSerreClass.lean, line 421. The attribute's comment: “proper support”.

[Stacks, Tag 0CYV], part (1). The coherent adic systems along ℐ whose first term has support proper over S form a Serre subcategory of Coh(X, ℐ).

All terms of a coherent adic system have the same support, and the support of the middle term of a short exact sequence is the union of the supports of the outer two, which is proper over S because a finite union of closed subsets proper over the base is proper over the base.

public theorem isSerreClass_hasProperSupport {X S : Scheme.{u}} [IsNoetherian S] (f : X ⟶ S)
    [LocallyOfFiniteType f] [QuasiCompact f] (I : X.IdealSheafData) :
    letI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian f
    letI : CompactSpace X := QuasiCompact.compactSpace_of_compactSpace f
    letI : IsNoetherian X := AlgebraicGeometry.IsNoetherian.mk
    ObjectProperty.IsSerreClass (C := CoherentAdicSystems I)
      (fun F => Stacks.Algebraization.HasProperSupport f (F.obj.obj (op 0)))

Stacks.Coherent.isSerreClass_hasProperAnnihilator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/ProperSerreClass.lean, line 471. The attribute's comment: “common proper annihilator”.

[Stacks, Tag 0CYV], part (2). The coherent adic systems along ℐ admitting a closed subscheme of X proper over S whose ideal sheaf annihilates every term form a Serre subcategory of Coh(X, ℐ).

An ideal sheaf annihilating every term of a system annihilates every term of a subobject and of a quotient; for an extension the product of the two ideal sheaves works, and the closed subset it cuts out is the union of the two, which is again proper over S.

public theorem isSerreClass_hasProperAnnihilator {X S : Scheme.{u}} [IsNoetherian S] (f : X ⟶ S)
    [LocallyOfFiniteType f] [QuasiCompact f] (I : X.IdealSheafData) :
    letI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian f
    letI : CompactSpace X := QuasiCompact.compactSpace_of_compactSpace f
    letI : IsNoetherian X := AlgebraicGeometry.IsNoetherian.mk
    (HasProperAnnihilator f I).IsSerreClass

Sources

• Section 30.26, Tag 0CYK
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.isProperOver_iff_exists_isProper · AlgebraicGeometry.exists_isProper_iff_forall_isProper · AlgebraicGeometry.IsProperOver · AlgebraicGeometry.isProperOver_of_le · AlgebraicGeometry.isProperOver_preimage_baseChange · AlgebraicGeometry.isClosed_image_of_isProperOver · AlgebraicGeometry.isProperOver_image · AlgebraicGeometry.isProperOver_preimage

Section30.27 Grothendieck's existence theorem, III#

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

Tag 088D, an equation

Tag 088D in the Stacks Project.

Stacks.Algebraization.completion_hasProperSupport, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionProper/Basic.lean, line 111. The attribute's comment: “proper support of the completion”.

Stacks 088D. The first term of the completion of a coherent sheaf whose support is proper over the base again has support proper over the base.

That term is the quotient F / I · F, so its support is a closed subset of the support of F, and a closed subset of a closed subset proper over the base is proper over the base.

public theorem completion_hasProperSupport
    (A : Type u) [CommRing A] [IsNoetherianRing A] (I : Ideal A)
    {X : Scheme.{u}} (f : X ⟶ Spec (.of A)) [LocallyOfFiniteType f]
    (F : CoherentModulesProperOver f) :
    letI : IsLocallyNoetherian X := LocallyOfFiniteType.isLocallyNoetherian f
    HasProperSupport f
      (((completionFunctor X (baseIdealSheaf A I f)).obj F.obj).obj.obj (op 0))

Stacks.Algebraization.completionFunctorProperOver, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionProper/Basic.lean, line 144. The attribute's comment: “the functor”.

Stacks 088D. The completion functor of Stacks 0880, restricted to the coherent sheaves and the coherent adic systems whose support is proper over the affine base.

public noncomputable def completionFunctorProperOver
    (A : Type u) [CommRing A] [IsNoetherianRing A] (I : Ideal A)
    {X : Scheme.{u}} (f : X ⟶ Spec (.of A)) [LocallyOfFiniteType f] :
    CoherentModulesProperOver f ⥤ CoherentAdicSystemsProperOver f (baseIdealSheaf A I f)

Tag 088E, a theorem

Tag 088E in the Stacks Project.

Stacks.Algebraization.isEquivalence_completionFunctorProperOver_holds, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionProper/AdicUnitConditionDescent.lean, line 343. The attribute's comment: “Grothendieck's existence theorem: A Noetherian and complete with respect to I, X separated and of finite type over A; the functor of 088D from coherent O_X-modules with support proper over A to coherent I-adic systems with support proper over A is an equivalence”. References: EGA III (5.2.5), “more general”; EGA III (5.2.6), “more general”.

[Stacks, Tag 088E], Grothendieck's existence theorem. Let A be a Noetherian ring complete with respect to an ideal I and let f : Z ⟶ Spec A be separated and of finite type (IsSeparated, LocallyOfFiniteType and QuasiCompact). Then the functor of [Stacks, Tag 088D]

Coh_{support proper over A}(𝒪_Z) ⥤ Coh_{support proper over A}(Z, I 𝒪_Z)

is an equivalence.

Stacks.Algebraization.isEquivalence_completionFunctorProperOver_of_adicBaseChangeUnitCondition at Stacks.Algebraization.hasAdicBaseChangeUnitCondition. Following the source, the proof reduces to Stacks 088C on the closed subschemes of Z proper over A, after showing that every coherent adic system with support proper over A is annihilated by the ideal sheaf of such a subscheme (Chow's lemma, the projective case 0885, and Stacks 088B through Stacks.Algebraization.transport_of_isDirectImageComparison).

This is the carrier of Stacks 088E: it takes no input beyond the source's hypotheses, and supersedes the conditional forms Stacks.Algebraization.isEquivalence_completionFunctorProperOver and Stacks.Algebraization.isEquivalence_completionFunctorProperOver_of_adicBaseChangeUnitCondition, which take theirs as an argument.

public theorem isEquivalence_completionFunctorProperOver_holds
    (A : Type u) [CommRing A] [IsNoetherianRing A] (I : Ideal A) [IsAdicComplete I A]
    {Z : Scheme.{u}} (f : Z ⟶ Spec (.of A))
    [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f] :
    (completionFunctorProperOver A I f).IsEquivalence

Tag 088F, a remark

Tag 088F in the Stacks Project.

AlgebraicGeometry.AdicCoherentModuleSystem, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AdicThickeningCoherentSystem.lean, line 143. The attribute's comment: “the systems (F n, phi n) of clauses (1), (2) and (3)”.

The systems (ℱₙ, φₙ) of Stacks 088F. For f : X ⟶ Spec A locally of finite type, a coherent 𝒪_{Xₙ}-module for every n, together with an isomorphism φₙ : iₙ^* ℱₙ₊₁ ≅ ℱₙ along the transition iₙ : Xₙ ⟶ Xₙ₊₁, whose first term has support proper over S₁.

The three fields other than obj are clauses (1), (2) and (3) of the remark. Clause (2) asks for an isomorphism as data, as in the source, not merely for the existence of one: the transition maps of the system are part of it.

public structure AdicCoherentModuleSystem (A : Type u) [CommRing A] (I : Ideal A)
    {X : Scheme.{u}} (f : X ⟶ Spec (.of A)) [LocallyOfFiniteType f]

AlgebraicGeometry.adicThickeningCompletionFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AdicThickeningCoherentSystem.lean, line 254. The attribute's comment: “the completion functor into those systems; not that it is an equivalence, for which Stacks 088E (itself conditional on 088C here) and an identification of the adic thickenings with the closed subschemes of the ideal powers are both missing”.

The completion functor of Stacks 088F. It sends a coherent 𝒪_X-module with support proper over A to the system (ℱ|_{Xₙ}) of its restrictions to the adic thickenings, with the transition isomorphisms induced by iₙ ≫ (Xₙ₊₁ ⟶ X) = (Xₙ ⟶ X), and a map of modules to the system of its restrictions.

This is the arrow displayed in the remark. That it is an equivalence is Stacks 088E read through an identification of the coherent adic systems of Stacks.Coherent.CoherentAdicSystems with the systems of this file; neither input is available in this library, so no equivalence is claimed here.

public def adicThickeningCompletionFunctor (A : Type u) [CommRing A] [IsNoetherianRing A]
    (I : Ideal A) {X : Scheme.{u}} (f : X ⟶ Spec (.of A)) [LocallyOfFiniteType f] :
    Stacks.Algebraization.CoherentModulesProperOver f ⥤ AdicCoherentModuleSystem A I f

AlgebraicGeometry.hasProperSupport_of_isProper_adicBaseChange, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AdicThickeningCoherentSystem.lean, line 283. The attribute's comment: “for a proper f the support condition (3) on the systems is vacuous”.

Stacks 088F, final clause: over a proper base the support conditions may be omitted. If f : X ⟶ Spec A is proper then the structure morphism Xₙ ⟶ Sₙ is proper too, being its base change, and so the support of any coherent 𝒪_{Xₙ}-module is proper over Sₙ. Hence clause (3) is automatic.

The companion statement on the other side of the arrow — that the support of any coherent 𝒪_X-module is then proper over A — is Stacks.Algebraization.hasProperSupport_of_isProper.

public lemma hasProperSupport_of_isProper_adicBaseChange [IsProper f] (n : ℕ)
    (F : (adicBaseChange A I f n).Modules) (hF : _root_.SheafOfModules.IsCoherent.{u} F) :
    HasProperSupport (pullback.snd f (adicThickeningι A I n)) F

AlgebraicGeometry.isEquivalence_adicThickeningCompletionFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionProper/AdicThickeningEssSurj.lean, line 245. The attribute's comment: “the completion functor from the coherent O_X-modules with support proper over A to the systems (F n, phi n) of clauses (1), (2) and (3) is an equivalence of categories, for A Noetherian and I-adically complete and X -> Spec A separated and of finite type”.

The completion functor is an equivalence. Let A be a Noetherian ring complete with respect to an ideal I, put S = Spec A, Sₙ = Spec (A / Iⁿ), let f : X ⟶ S be separated and of finite type (locally of finite type and quasi-compact) and Xₙ = X ×_S Sₙ. Then the completion functor AlgebraicGeometry.adicThickeningCompletionFunctor, from the coherent 𝒪_X-modules with support proper over A to the systems (ℱₙ, φₙ) — ℱₙ coherent on Xₙ, φₙ : iₙ^*ℱₙ₊₁ ≅ ℱₙ, and Supp(ℱ₁) proper over S₁ — sending ℱ to its restrictions ℱ|_{Xₙ}, is an equivalence of categories.

public theorem isEquivalence_adicThickeningCompletionFunctor
    (A : Type u) [CommRing A] [IsNoetherianRing A] (I : Ideal A) [IsAdicComplete I A]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of A))
    [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f] :
    (adicThickeningCompletionFunctor A I f).IsEquivalence

AlgebraicGeometry.isEquivalence_adicThickeningTransitionCompletionFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionProper/AdicThickeningProperEquivalence.lean, line 190. The attribute's comment: “the special case of X proper over A, with the conditions on the supports omitted: completion from all coherent O_X-modules to the systems of coherent O_{X_n}-modules F n with isomorphisms phi n is an equivalence of categories”.

Let A be a Noetherian ring complete with respect to an ideal I, let f : X ⟶ Spec A be proper and Xₙ = X ×_S Sₙ. Then completion ℱ ↦ (ℱ|_{Xₙ}) is an equivalence from the category of all coherent 𝒪_X-modules to the category of systems (ℱₙ, φₙ) with ℱₙ a coherent 𝒪_{Xₙ}-module and φₙ : iₙ^*ℱₙ₊₁ ≅ ℱₙ an isomorphism.

public theorem isEquivalence_adicThickeningTransitionCompletionFunctor [IsNoetherianRing A]
    [IsAdicComplete I A] [IsProper f] :
    (adicThickeningTransitionCompletionFunctor A I f).IsEquivalence

Sources

• Section 30.27, Tag 0CYW
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Algebraization.completion_hasProperSupport · Stacks.Algebraization.completionFunctorProperOver · Stacks.Algebraization.isEquivalence_completionFunctorProperOver_holds · AlgebraicGeometry.AdicCoherentModuleSystem · AlgebraicGeometry.adicThickeningCompletionFunctor · AlgebraicGeometry.hasProperSupport_of_isProper_adicBaseChange · AlgebraicGeometry.isEquivalence_adicThickeningCompletionFunctor · AlgebraicGeometry.isEquivalence_adicThickeningTransitionCompletionFunctor

Section30.28 Grothendieck's algebraization theorem#

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

Tag 0899, a lemma

Tag 0899 in the Stacks Project.

AlgebraicGeometry.exists_closedImmersion_algebraization_of_isPullback_holds, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionProper/AdicFiniteAlgebraizationTags.lean, line 161. The attribute's comment: “at the source's hypotheses and with no further input: A Noetherian and I-adically complete, f : X -> Spec A separated of finite type (IsSeparated, LocallyOfFiniteType and QuasiCompact), a system j n : Z n -> X n with cartesian transition squares whose j 0 is a closed immersion (source hypothesis 1) and whose Z 0 -> S 0 is proper (source hypothesis 2), concluding a closed immersion g : W -> X with W proper over Spec A recovering the system by base change. The halg binder of AlgebraicGeometry.exists_closedImmersion_algebraization_of_isPullback is discharged here, by AlgebraicGeometry.adicFiniteSystemAlgebraization_of_adicFiniteAlgebraAlgebraization at AlgebraicGeometry.adicFiniteAlgebraAlgebraization_holds”.

Algebraization of a cartesian system of closed immersions over the adic thickenings. Let A be a Noetherian ring complete with respect to an ideal I, write S = Spec A and Sₙ = Spec (A / Iⁿ), and let f : X ⟶ S be separated of finite type; put Xₙ = X ×_S Sₙ. Given a system of morphisms jₙ : Zₙ ⟶ Xₙ with transition maps making every square over Xₙ ⟶ Xₙ₊₁ cartesian, with j 0 : Z₀ ⟶ X₀ a closed immersion and Z₀ ⟶ S₀ proper, there is a closed immersion g : W ⟶ X with W proper over S recovering the system by base change.

public theorem exists_closedImmersion_algebraization_of_isPullback_holds
    (A : Type u) [CommRing A] [IsNoetherianRing A] (I : Ideal A)
    (hcomplete : IsAdicComplete I A) {X : Scheme.{u}} (f : X ⟶ Spec (.of A))
    [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f]
    (Z : ℕ → Scheme.{u}) (j : ∀ n, Z n ⟶ adicBaseChange A I f n) (t : ∀ n, Z n ⟶ Z (n + 1))
    (hcart : ∀ n, IsPullback (t n) (j n) (j (n + 1)) (adicBaseChangeSucc A I f n))
    (hclosed : IsClosedImmersion (j 0))
    (hproper : IsProper (j 0 ≫ pullback.snd f (adicThickeningι A I 0))) :
    ∃ (W : Scheme.{u}) (g : W ⟶ X) (k : ∀ n, Z n ⟶ W),
      IsClosedImmersion g ∧ IsProper (g ≫ f) ∧
      (∀ n, IsPullback (k n) (j n ≫ pullback.snd f (adicThickeningι A I n)) (g ≫ f)
        (adicThickeningι A I n)) ∧
      (∀ n, k n ≫ g = j n ≫ pullback.fst f (adicThickeningι A I n)) ∧
      ∀ n, t n ≫ k (n + 1) = k n

AlgebraicGeometry.exists_closedImmersion_algebraization_of_isPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/FormalClosedSubschemeAlgebraization.lean, line 354. The attribute's comment: “with Stacks 09ZT as the hypothesis halg and the uniqueness clause of Stacks 0A42 as the hypothesis hrig”.

Stacks Project, Tag 0899. Let A be a Noetherian ring complete with respect to an ideal I, write S = Spec A and Sₙ = Spec (A / Iⁿ), and let f : X ⟶ S be separated of finite type. Put Xₙ = X ×_S Sₙ. Suppose given a system of morphisms jₙ : Zₙ ⟶ Xₙ together with transition maps tₙ : Zₙ ⟶ Z_{n+1} making every square

  Zₙ --tₙ--> Z_{n+1}
  |            |
  Xₙ --iₙ--> X_{n+1}

cartesian, and assume that j 0 : Z₀ ⟶ X₀ is a closed immersion and that Z₀ ⟶ S₀ is proper. Then there is a closed immersion g : Z ⟶ X with Z proper over S which recovers the given system by base change: each Zₙ is Z ×_S Sₙ, the morphism Zₙ ⟶ X is jₙ followed by the projection Xₙ ⟶ X, and the transition maps tₙ are compatible with the identifications.

The hypotheses are the source's: f is only separated of finite type, and it is the closed member Z₀ ⟶ S₀ of the system, not f, that is proper.

The proof is the source's, in the form in which it is available here. Stacks 0896 upgrades the closed immersion j 0 to a closed immersion jₙ for every n (isClosedImmersion_of_isPullback_adicBaseChangeSucc); each jₙ is therefore finite, so Stacks 09ZT — the hypothesis halg — algebraizes the system to a finite g : Z ⟶ X with Z proper over S; and g is a monomorphism, hence a closed immersion, by rigidity — the hypothesis hrig, the uniqueness clause of Stacks 0A42. Neither halg nor hrig is carried by this library; see the module documentation. The Noetherian and completeness hypotheses on A are the ones under which halg and hrig hold, and IsNoetherianRing A is moreover used directly, to see that the transition maps of the adic system are of finite presentation.

public theorem exists_closedImmersion_algebraization_of_isPullback [IsNoetherianRing A]
    (hcomplete : IsAdicComplete I A) (halg : AdicFiniteSystemAlgebraization A I f)
    (hrig : AdicMorphismRigidity A I) [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f]
    (Z : ℕ → Scheme.{u}) (j : ∀ n, Z n ⟶ adicBaseChange A I f n) (t : ∀ n, Z n ⟶ Z (n + 1))
    (hcart : ∀ n, IsPullback (t n) (j n) (j (n + 1)) (adicBaseChangeSucc A I f n))
    (hclosed : IsClosedImmersion (j 0))
    (hproper : IsProper (j 0 ≫ pullback.snd f (adicThickeningι A I 0))) :
    ∃ (W : Scheme.{u}) (g : W ⟶ X) (k : ∀ n, Z n ⟶ W),
      IsClosedImmersion g ∧ IsProper (g ≫ f) ∧
      (∀ n, IsPullback (k n) (j n ≫ pullback.snd f (adicThickeningι A I n)) (g ≫ f)
        (adicThickeningι A I n)) ∧
      (∀ n, k n ≫ g = j n ≫ pullback.fst f (adicThickeningι A I n)) ∧
      ∀ n, t n ≫ k (n + 1) = k n

Tag 09ZT, a lemma

Tag 09ZT in the Stacks Project.

AlgebraicGeometry.exists_finite_algebraization_of_adicFiniteSystem_holds, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionProper/AdicFiniteAlgebraizationTags.lean, line 97. The attribute's comment: “at the source's hypotheses and with no further input: A Noetherian and I-adically complete, f : X -> Spec A separated of finite type (IsSeparated, LocallyOfFiniteType and QuasiCompact), a system (Y n) of schemes over the adic thickenings with cartesian transition squares, every Y n -> X n finite (source hypothesis 1) and Y 0 -> S 0 proper (source hypothesis 2), concluding the finite algebraization a : Z -> X proper over Spec A with every Y n the fibre product Z x_S S n. The halg binder of AlgebraicGeometry.exists_finite_algebraization_of_adicFiniteSystem is discharged here, by AlgebraicGeometry.adicFiniteAlgebraAlgebraization_holds”.

Algebraization of a cartesian system of finite schemes over the adic thickenings. Let A be a Noetherian ring complete with respect to an ideal I, write S = Spec A and Sₙ = Spec (A / Iⁿ), and let f : X ⟶ S be separated of finite type; put Xₙ = X ×_S Sₙ. Let (Yₙ) be a system of schemes over the Xₙ whose squares over the transitions Xₙ ⟶ Xₙ₊₁ are cartesian, with every Yₙ ⟶ Xₙ finite and Y₀ ⟶ S₀ proper. Then there is a finite morphism a : Z ⟶ X which is proper over S and maps kₙ : Yₙ ⟶ Z over X exhibiting every Yₙ as the fibre product Z ×_S Sₙ.

public theorem exists_finite_algebraization_of_adicFiniteSystem_holds
    (A : Type u) [CommRing A] [IsNoetherianRing A] (I : Ideal A) [IsAdicComplete I A]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of A))
    [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f]
    (Y : ℕ → Scheme.{u}) (y : ∀ n, Y n ⟶ adicBaseChange A I f n)
    (t : ∀ n, Y n ⟶ Y (n + 1))
    (hcart : ∀ n, IsPullback (t n) (y n) (y (n + 1)) (adicBaseChangeSucc A I f n))
    (hfin : ∀ n, IsFinite (y n))
    (hproper : IsProper (y 0 ≫ pullback.snd f (adicThickeningι A I 0))) :
    ∃ (Z : Scheme.{u}) (a : Z ⟶ X), IsFinite a ∧ IsProper (a ≫ f) ∧
      ∃ k : ∀ n, Y n ⟶ Z,
        (∀ n, IsPullback (k n) (y n ≫ pullback.snd f (adicThickeningι A I n)) (a ≫ f)
          (adicThickeningι A I n)) ∧
        ∀ n, k n ≫ a = y n ≫ pullback.fst f (adicThickeningι A I n)

AlgebraicGeometry.exists_finite_algebraization_of_adicFiniteSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/FiniteAlgebraization.lean, line 215. The attribute's comment: “with Grothendieck existence for finite sheaves of algebras (088F for the underlying coherent module and 088E for the algebra structure, both resting on 088C, which this library does not carry) as the hypothesis halg”.

Stacks Project, Tag 09ZT. Let A be a Noetherian ring complete with respect to an ideal I, write S = Spec A and Sₙ = Spec (A / Iⁿ), and let f : X ⟶ S be separated of finite type; put Xₙ = X ×_S Sₙ. Let (Yₙ) be a system of schemes over the Xₙ whose squares over the transitions Xₙ ⟶ Xₙ₊₁ are cartesian, with every Yₙ ⟶ Xₙ finite and Y₀ ⟶ S₀ proper. Then there is a finite morphism a : Y ⟶ X which is proper over S and maps kₙ : Yₙ ⟶ Y over X exhibiting every Yₙ as the fibre product Y ×_S Sₙ.

The proof is the source's, read through the anti-equivalence between schemes affine over a base and quasi-coherent sheaves of algebras (Stacks 01S8, 01SA): the pushforward algebras f_{n,*}𝒪_{Yₙ} are finite, the cartesian squares identify the pullback of the (n+1)-st with the n-th (Stacks 01LX part 2), so the hypothesis halg algebraizes them to a finite quasi-coherent algebra C on X proper over S, and Y = Spec_X(C) is finite over X with Y ×_X Xₙ = Spec_{Xₙ}(C|_{Xₙ}) = Yₙ; pasting that square with Xₙ = X ×_S Sₙ gives Yₙ = Y ×_S Sₙ.

The Noetherian and completeness hypotheses on A are exactly the ones under which halg holds, and are kept in the statement for that reason.

public theorem exists_finite_algebraization_of_adicFiniteSystem
    (A : Type u) [CommRing A] [IsNoetherianRing A] (I : Ideal A) [IsAdicComplete I A]
    {X : Scheme.{u}} (f : X ⟶ Spec (.of A))
    [IsSeparated f] [LocallyOfFiniteType f] [QuasiCompact f]
    (halg : AdicFiniteAlgebraAlgebraization A I f)
    (Y : ℕ → Scheme.{u}) (y : ∀ n, Y n ⟶ adicBaseChange A I f n)
    (t : ∀ n, Y n ⟶ Y (n + 1))
    (hcart : ∀ n, IsPullback (t n) (y n) (y (n + 1)) (adicBaseChangeSucc A I f n))
    (hfin : ∀ n, IsFinite (y n))
    (hproper : IsProper (y 0 ≫ pullback.snd f (adicThickeningι A I 0))) :
    ∃ (Z : Scheme.{u}) (a : Z ⟶ X), IsFinite a ∧ IsProper (a ≫ f) ∧
      ∃ k : ∀ n, Y n ⟶ Z,
        (∀ n, IsPullback (k n) (y n ≫ pullback.snd f (adicThickeningι A I n)) (a ≫ f)
          (adicThickeningι A I n)) ∧
        ∀ n, k n ≫ a = y n ≫ pullback.fst f (adicThickeningι A I n)

AlgebraicGeometry.adicFiniteAlgebraization_of_adicFiniteAlgebraAlgebraization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/FiniteAlgebraization.lean, line 284. The attribute's comment: “in the packaging AdicFiniteAlgebraization, with Grothendieck existence for finite sheaves of algebras (088F, 088E, resting on 088C) as the hypothesis halg”.

Stacks 09ZT in the packaging that Stacks 0A42 consumes. The hypothesis AlgebraicGeometry.AdicFiniteAlgebraization of AlgebraicGeometry.existsUnique_algebraization_adicBaseChangeMap is exactly the conclusion of exists_finite_algebraization_of_adicFiniteSystem with the finiteness of the algebraized morphism forgotten, so the latter discharges it.

public theorem adicFiniteAlgebraization_of_adicFiniteAlgebraAlgebraization
    (A : Type u) [CommRing A] [IsNoetherianRing A] (I : Ideal A) [IsAdicComplete I A]
    (halg : ∀ {P : Scheme.{u}} (fP : P ⟶ Spec (.of A)),
      AdicFiniteAlgebraAlgebraization A I fP) :
    AdicFiniteAlgebraization A I

Tag 0A42, a lemma

Tag 0A42 in the Stacks Project.

AlgebraicGeometry.existsUnique_algebraization_adicBaseChangeMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/AlgebraizeMorphism.lean, line 383. The attribute's comment: “with Stacks 09ZT as the hypothesis halg and the rigidity consequence of Grothendieck existence (088C, via 0883) as the hypothesis hrig”.

Stacks Project, Tag 0A42. Let A be a Noetherian ring complete with respect to an ideal I, write S = Spec A and Sₙ = Spec (A / Iⁿ), and let fX : X ⟶ S be proper and fY : Y ⟶ S separated of finite type. A compatible system of morphisms gₙ : Xₙ ⟶ Yₙ over Sₙ — one for every n ≥ 1, with every composite Xₙ ⟶ X_{n+1} ⟶ Y_{n+1} equal to Xₙ ⟶ Yₙ ⟶ Y_{n+1} — comes from a unique morphism g : X ⟶ Y over S whose base change to each Sₙ is gₙ.

The proof is the source's: the graphs of the gₙ are closed immersions Xₙ ⟶ (X ×_S Y)ₙ because fY is separated, Stacks 09ZT algebraizes them to a closed subscheme Z ⊆ X ×_S Y proper over S (the hypothesis halg), the first projection p : Z ⟶ X has all its adic base changes isomorphisms and is therefore an isomorphism, and g is inv p ≫ q. Both that last step and the uniqueness clause rest on adic rigidity over a proper base (the hypothesis hrig), the consequence of Grothendieck existence used by the source.

Neither halg (Stacks 09ZT) nor hrig is carried by this library; see the module documentation. The Noetherian and completeness hypotheses on A are exactly the ones under which halg and hrig hold, and are kept in the statement for that reason.

public theorem existsUnique_algebraization_adicBaseChangeMap
    [IsNoetherianRing A] (hcomplete : IsAdicComplete I A)
    (halg : AdicFiniteAlgebraization A I) (hrig : AdicRigidity A I)
    (fX : X ⟶ Spec (.of A)) (fY : Y ⟶ Spec (.of A))
    [IsProper fX] [IsSeparated fY] [LocallyOfFiniteType fY] [QuasiCompact fY]
    (g : ∀ n, adicBaseChange A I fX n ⟶ adicBaseChange A I fY n)
    (g_over : ∀ n, g n ≫ pullback.snd fY (adicThickeningι A I n) =
      pullback.snd fX (adicThickeningι A I n))
    (g_compatible : ∀ n, adicBaseChangeSucc A I fX n ≫ g (n + 1) =
      g n ≫ adicBaseChangeSucc A I fY n) :
    ∃! algebraization : {h : X ⟶ Y // h ≫ fY = fX},
      ∀ n, adicBaseChangeMap A I algebraization.1 algebraization.2 n = g n

AlgebraicGeometry.existsUnique_algebraization_adicBaseChangeMap_holds, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/CompletionProper/AdicFiniteAlgebraizationTags.lean, line 127. The attribute's comment: “at the source's hypotheses and with no further input: A Noetherian and I-adically complete, fX : X -> Spec A proper (source hypothesis 1), fY : Y -> Spec A separated of finite type (source hypothesis 2), and a compatible system of morphisms over the adic thickenings, concluding that it comes from a unique morphism X -> Y over Spec A. The halg binder of AlgebraicGeometry.existsUnique_algebraization_adicBaseChangeMap is discharged here, by AlgebraicGeometry.adicFiniteAlgebraization_holds”.

Algebraization of a compatible system of morphisms over the adic thickenings. Let A be a Noetherian ring complete with respect to an ideal I, write S = Spec A and Sₙ = Spec (A / Iⁿ), and let fX : X ⟶ S be proper and fY : Y ⟶ S separated of finite type. A compatible system of morphisms gₙ : Xₙ ⟶ Yₙ over Sₙ comes from a unique morphism g : X ⟶ Y over S whose base change to each Sₙ is gₙ.

public theorem existsUnique_algebraization_adicBaseChangeMap_holds
    (A : Type u) [CommRing A] [IsNoetherianRing A] (I : Ideal A)
    (hcomplete : IsAdicComplete I A) {X Y : Scheme.{u}}
    (fX : X ⟶ Spec (.of A)) (fY : Y ⟶ Spec (.of A))
    [IsProper fX] [IsSeparated fY] [LocallyOfFiniteType fY] [QuasiCompact fY]
    (g : ∀ n, adicBaseChange A I fX n ⟶ adicBaseChange A I fY n)
    (g_over : ∀ n, g n ≫ pullback.snd fY (adicThickeningι A I n) =
      pullback.snd fX (adicThickeningι A I n))
    (g_compatible : ∀ n, adicBaseChangeSucc A I fX n ≫ g (n + 1) =
      g n ≫ adicBaseChangeSucc A I fY n) :
    ∃! algebraization : {h : X ⟶ Y // h ≫ fY = fX},
      ∀ n, adicBaseChangeMap A I algebraization.1 algebraization.2 n = g n

Tag 089A, a theorem

Tag 089A in the Stacks Project.

Stacks.GrothendieckAlgebraization.exists_isProper_isAmple_algebraization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/FormalGeometry/GrothendieckAlgebraization.lean, line 67.

Grothendieck's algebraization theorem, [Stacks, Tag 089A].

Let A be a Noetherian ring complete with respect to an ideal I, let Xₙ be a tower of schemes over the thickenings Sₙ = Spec (A / Iⁿ⁺¹) with transitions iₙ : Xₙ ⟶ Xₙ₊₁ whose squares over Sₙ ⟶ Sₙ₊₁ are cartesian, and let ℒₙ be invertible modules on the Xₙ with isomorphisms φₙ : iₙ^* ℒₙ₊₁ ≅ ℒₙ. If X₀ ⟶ S₀ is proper and ℒ₀ is ample on X₀, then there are a proper morphism fX : X ⟶ Spec A, an ample invertible 𝒪_X-module ℒ, morphisms kₙ : Xₙ ⟶ X with iₙ ≫ kₙ₊₁ = kₙ exhibiting every Xₙ as X ×_{Spec A} Sₙ, and isomorphisms ℒₙ ≅ ℒ|_{Xₙ} compatible with the φₙ.

public theorem exists_isProper_isAmple_algebraization (A : Type u) [CommRing A]
    [IsNoetherianRing A] (I : Ideal A) [IsAdicComplete I A] {Xn : ℕ → Scheme.{u}}
    (q : ∀ n, Xn n ⟶ adicThickening A I n) (i : ∀ n, Xn n ⟶ Xn (n + 1))
    (hcart : ∀ n, IsPullback (i n) (q n) (q (n + 1)) (adicThickeningSucc A I n))
    (L : ∀ n, (Xn n).Modules) (hL : ∀ n, IsInvertibleModule (Xn n) (L n))
    (φ : ∀ n, (Scheme.Modules.pullback (i n)).obj (L (n + 1)) ≅ L n)
    (hproper : IsProper (q 0))
    (hample : letI := hL 0; IsAmple (Xn 0) (L 0)) :
    ∃ (X : Scheme.{u}) (fX : X ⟶ Spec (.of A)), IsProper fX ∧
      ∃ (M : X.Modules) (hM : IsInvertibleModule X M), @IsAmple X M hM ∧
        ∃ (k : ∀ n, Xn n ⟶ X) (hk : ∀ n, i n ≫ k (n + 1) = k n),
          (∀ n, IsPullback (k n) (q n) fX (adicThickeningι A I n)) ∧
          ∃ e : ∀ n, L n ≅ (Scheme.Modules.pullback (k n)).obj M,
            ∀ n, (φ n).hom ≫ (e n).hom =
              (Scheme.Modules.pullback (i n)).map (e (n + 1)).hom ≫
                (Scheme.Modules.pullbackComp (i n) (k (n + 1))).hom.app M ≫
                  (Scheme.Modules.pullbackCongr (hk n)).hom.app M

Sources

• Section 30.28, Tag 0898
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.exists_closedImmersion_algebraization_of_isPullback_holds · AlgebraicGeometry.exists_closedImmersion_algebraization_of_isPullback · AlgebraicGeometry.exists_finite_algebraization_of_adicFiniteSystem_holds · AlgebraicGeometry.exists_finite_algebraization_of_adicFiniteSystem · AlgebraicGeometry.adicFiniteAlgebraization_of_adicFiniteAlgebraAlgebraization · AlgebraicGeometry.existsUnique_algebraization_adicBaseChangeMap · AlgebraicGeometry.existsUnique_algebraization_adicBaseChangeMap_holds · Stacks.GrothendieckAlgebraization.exists_isProper_isAmple_algebraization

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.