69.16 Vanishing of cohomology to 69.23 Applications of the…

Section69.16 Vanishing of cohomology #

Section 69.16 of the Stacks Project, Tag 07UX. 9 tags here are carried by 18 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 07UY, a situation

Tag 07UY in the Stacks Project.

AlgebraicGeometry.Space.CohomologyVanishingSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohomologyVanishing.lean, line 75.

Stacks 07UY. A quasi-compact, quasi-separated algebraic space X over a scheme S every one of whose quasi-coherent modules has vanishing first cohomology.

structure CohomologyVanishingSituation

Tag 07UZ, a lemma

Tag 07UZ in the Stacks Project.

AlgebraicGeometry.Space.CohomologyVanishingSituation.isIso_unit_tensorSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohomologyVanishingTensorStructureSheaf.lean, line 360. The attribute's comment: “first assertion: p_(M ⊗_A 𝒪_X) = M~, the unit M~ ⟶ p_p^M~ of the adjunction p^ ⊣ p_* being an isomorphism”.

Stacks 07UZ, first assertion: p_*(M ⊗_A 𝒪_X) = M~. In Situation 07UY, for every A-module M, the unit M~ ⟶ p_*p^*M~ = p_*(M ⊗_A 𝒪_X) of the adjunction p^* ⊣ p_* of Stacks 03LU is an isomorphism.

p is an isomorphism (…CohomologyVanishingSituation.isIso_toSpecA), so p^* is fully faithful and the unit is invertible.

theorem isIso_unit_tensorSheaf :
    IsIso ((modulePullbackAdjunction T.site (⊤_ Scheme.{u}) T.containsTerminal T.toSpecA).unit.app
      (T.tildeModule M))

AlgebraicGeometry.Space.CohomologyVanishingSituation.globalSectionsTensorLinearEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohomologyVanishingTensorStructureSheaf.lean, line 688. The attribute's comment: “second assertion: Γ(X, M ⊗_A 𝒪_X) = M, as A-modules”.

Stacks 07UZ, second assertion: Γ(X, M ⊗_A 𝒪_X) = M. In Situation 07UY, for every A-module M, the global sections of M ⊗_A 𝒪_X = p^*M~ are M, as A-modules, the global sections being a module over A = Γ(X, 𝒪_X).

It is M = Γ(Spec A, M~) = Γ(Spec A, p_*p^*M~) = Γ(X, p^*M~), the middle step being the first assertion …CohomologyVanishingSituation.isIso_unit_tensorSheaf and the last Stacks 0732.

def globalSectionsTensorLinearEquiv :
    M ≃ₗ[T.globalFunctions]
      (ModuleCat.restrictScalars T.globalFunctionsOverIntegersEquiv.toRingHom).obj
        (T.spaceSections M)

Stacks.Cohomology.SiteModules.sectionTensorFreeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/FreeTensorStructureSheaf.lean, line 210. The attribute's comment: “the case of a free module: (⨁_I A) ⊗_A 𝒪_X is the free sheaf of modules on I”.

The tensor of a free module over the global functions with the structure sheaf is the free sheaf of modules on the same index set: (⨁_I A) ⊗_A 𝒪 ≅ 𝒪^{(I)}.

Both sides corepresent the functor F ↦ (I → Γ(C, F)), and the isomorphism compares the two corepresenting objects.

def sectionTensorFreeIso (I : Type (max u r)) :
    (sectionTensorSheafFunctor.{u, v, max u r, u} O).obj (freeGlobalModule O I) ≅
      SheafOfModules.free (R := ringSheafOfSite O) I

Stacks.Cohomology.SiteModules.sectionTensorSheafAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/GlobalSectionsTensor.lean, line 633. The attribute's comment: “the module M ⊗_A 𝒪_X of the statement, as the left adjoint of global sections”.

The functor M ↦ M ⊗_A 𝒪 is left adjoint to global sections.

Consequently it preserves all colimits; in particular it is right exact, which is what a presentation of M by free A-modules is used for.

def sectionTensorSheafAdjunction :
    sectionTensorSheafFunctor O ⊣ globalSectionsFunctor (ringSheafOfSite O)

Stacks.Cohomology.SiteModules.isIso_sectionTensorSheafUnit_free, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/SectionTensorGlobalSections.lean, line 343. The attribute's comment: “the free-module case of Γ(X, M ⊗_A 𝒪_X) = M, i.e. the direct-sum computation Γ(X, ⨁_I 𝒪_X) = ⨁_I A, granted that global sections commute with that direct sum”.

Γ(C, (⨁_I A) ⊗_A 𝒪) = ⨁_I A, granted that the global-sections functor commutes with the coproduct of I copies of the structure sheaf.

The canonical map factors as the comparison ⨁_I A ⟶ Γ(C, 𝒪^{(I)}) through the global sections of the isomorphism (⨁_I A) ⊗_A 𝒪 ≅ 𝒪^{(I)}, and that comparison is invertible because Γ(C, ⨁_{i ∈ I} 𝒪) = ⨁_{i ∈ I} A.

theorem isIso_sectionTensorSheafUnit_free (I : Type (max u r))
    (hI : PreservesColimit
      (Discrete.functor (fun _ : I => SheafOfModules.unit (ringSheafOfSite O)))
      (globalSectionsFunctor.{u, v, max u r, max u r} (ringSheafOfSite O))) :
    IsIso (sectionTensorSheafUnit.{u, v, max u r, u} (freeGlobalModule O I))

Stacks.Cohomology.SiteModules.isQuasicoherentOnSite_sectionTensor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/SectionTensorPresentation.lean, line 253. The attribute's comment: “quasi-coherence of the module M ⊗_A 𝒪_X attached to a module over the global functions”.

M ⊗_A 𝒪 is quasi-coherent on the site for every module M over the global functions. It is the cokernel of a map of free sheaves of O-modules, which is a global presentation.

theorem isQuasicoherentOnSite_sectionTensor (M : ModuleCat.{max u r} (GlobalFunctionRing O)) :
    ((sectionTensorSheafFunctor.{u, v, max u r, u} O).obj M).IsQuasicoherentOnSite

Tag 07V0, a lemma

Tag 07V0 in the Stacks Project.

AlgebraicGeometry.Space.CohomologyVanishingSituation.isZero_rightDerived_one_globalSectionsFunctor_of_isAffineHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohomologyVanishingAffineMorphism.lean, line 120. The attribute's comment: “part (1); cohomology of modules at the universe of the structure sheaf”.

Clause (1) of Stacks 07V0. In the situation of Stacks 07UY, let f : X' ⟶ X be an affine morphism of algebraic spaces and let 𝓕' be a quasi-coherent 𝒪_{X'}-module. Then H¹(X', 𝓕') = 0.

theorem isZero_rightDerived_one_globalSectionsFunctor_of_isAffineHom
    {X' : AlgebraicSpaces T.site T.base T.containsBase} (f : X' ⟶ T.space)
    (hf : IsAffineHom T.site T.base T.containsBase f.hom)
    (F : Modules.{u, u} T.site T.base T.containsBase X'.1 X'.2)
    (hF : F.IsQuasicoherentOnSite) :
    have := enoughInjectives_modules T.site T.base T.containsBase X'.1 X'.2
    IsZero (((globalSectionsFunctor.{u + 1, u, u, u} (Stacks.SheafOfModules.Tensor.ringSheaf
      (smallEtaleRingedSite T.site T.base T.containsBase X'.1 X'.2).O)).rightDerived 1).obj F)

AlgebraicGeometry.Space.CohomologyVanishingSituation.isAffineHom_of_isPullback_toSpecGlobalFunctions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohomologyVanishingBaseChange.lean, line 133. The attribute's comment: “clause (2), the affineness assertion only: the projection X ×_{Spec A} Spec A' → X is affine. The computation Γ(X', 𝒪_{X'}) = A' of the same clause is NOT proved -- it needs the pushforward-computation assertion of Stacks 07U8, which the library's form of that tag does not carry. See this file's implementation notes, and for clause (1) see StacksFrontier/AlgebraicGeometry/Spaces/CohomologyVanishingAffine.lean”.

The affineness assertion of clause (2) of Stacks 07V0. Let X be as in Stacks 07UY, let A = Γ(X, 𝒪_X), and let A' be an A-algebra, presented by a morphism q : W ⟶ V of affine objects of the site over the presentation of Spec A. Then the projection X' = X ×_{Spec A} Spec A' ⟶ X is affine.

A morphism of affine objects of the site is an affine morphism of algebraic spaces, and affine morphisms are stable under base change, which is Stacks 03WI.

theorem isAffineHom_of_isPullback_toSpecGlobalFunctions
    {W : BigFppfOver T.site T.base T.containsBase}
    [IsAffine ((BigFppfOver.toScheme T.site T.base T.containsBase).obj W)]
    (q : W ⟶ V) {X' : AlgebraicSpaces T.site T.base T.containsBase}
    {pr : X' ⟶ T.space} {pr' : X' ⟶ _root_.AlgebraicGeometry.schemeSpace W}
    (sq : IsPullback pr' pr (_root_.AlgebraicGeometry.schemeSpaceMap q)
      (toSpecGlobalFunctions T hterminal V e)) :
    IsAffineHom T.site T.base T.containsBase pr.hom

AlgebraicGeometry.Space.CohomologyVanishingSituation.isAffineHom_and_bijective_of_isPullback_toSpecGlobalFunctionsOverIntegers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohomologyVanishingBaseChangeGlobalFunctions.lean, line 168. The attribute's comment: “part (2); Spec A' is an affine object W of the site over the presentation V of Spec A”.

Clause (2) of Stacks 07V0. Let X be as in Stacks 07UY, let A = Γ(X, 𝒪_X), and let A' be an A-algebra, presented by a morphism q : W ⟶ V of affine objects of the site over the presentation V of Spec A. Then the projection X' = X ×_{Spec A} Spec A' ⟶ X is affine and the canonical map A' = Γ(W, 𝒪_W) ⟶ Γ(X', 𝒪_{X'}) is a bijection.

theorem isAffineHom_and_bijective_of_isPullback_toSpecGlobalFunctionsOverIntegers
    {W : BigFppfOver T.site (⊤_ Scheme.{u}) T.containsTerminal}
    [IsAffine ((BigFppfOver.toScheme T.site (⊤_ Scheme.{u}) T.containsTerminal).obj W)]
    (q : W ⟶ V) {X' : AlgebraicSpaces T.site (⊤_ Scheme.{u}) T.containsTerminal}
    {pr : X' ⟶ T.spaceOverIntegers} {pr' : X' ⟶ _root_.AlgebraicGeometry.schemeSpace W}
    (sq : IsPullback pr' pr (_root_.AlgebraicGeometry.schemeSpaceMap q)
      (toSpecGlobalFunctionsOverIntegers T V e)) :
    IsAffineHom T.site (⊤_ Scheme.{u}) T.containsTerminal pr.hom ∧
      Function.Bijective
        (pullbackToGlobalFunctions T.site (⊤_ Scheme.{u}) T.containsTerminal X' W pr')

Tag 07V1, a lemma

Tag 07V1 in the Stacks Project.

AlgebraicGeometry.exists_sub_one_mem_vanishingIdeal_of_disjoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohomologyVanishingSeparation.lean, line 335. The attribute's comment: “the conclusion for an affine scheme, with the two closed subsets taken in the scheme rather than in the points of an algebraic space”.

Two disjoint closed subsets of an affine scheme are separated by a global function. The vanishing ideals of the two sets are comaximal, because the support of their join is the intersection of the two sets, so 1 is a sum a + b with a vanishing on the first set and b on the second; then a - 1 = -b vanishes on the second.

theorem exists_sub_one_mem_vanishingIdeal_of_disjoint (X : Scheme.{u}) [IsAffine X]
    {T₀ T₁ : Set X} (hT₀ : IsClosed T₀) (hT₁ : IsClosed T₁) (hdisj : Disjoint T₀ T₁) :
    ∃ a : Γ(X, ⊤), T₀ ⊆ X.zeroLocus {a} ∧ T₁ ⊆ X.zeroLocus {a - 1}

AlgebraicGeometry.Space.CohomologyVanishingSituation.exists_subset_compl_sectionSupport_of_disjoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohomologyVanishingSeparation.lean, line 768. The attribute's comment: “the conclusion for an algebraic space, with the cohomology-vanishing hypothesis of Situation 07UY imposed at the module universe of the structure sheaf rather than at a general module universe”.

Stacks 07V1 for an algebraic space. In the situation of Stacks 07UY, two disjoint closed subsets Z₀, Z₁ of the points of X are separated by a global regular function: there is a ∈ A = Γ(X, 𝒪_X) with Z₀ ⊆ V(a) and Z₁ ⊆ V(a - 1). The vanishing locus V(-) is the complement of AlgebraicGeometry.Space.sectionSupport, the set of points at which a global function does not vanish.

The function is produced by AlgebraicGeometry.Space.CohomologyVanishingSituation.exists_mem_definingIdealAt_and_sub_one_mem applied to the reduced closed subspaces of Stacks 03IQ on Z₀, on Z₁ and on Z₀ ∪ Z₁. Its two hypotheses are exactly the two statements about the defining ideal sheaves of reduced closed subspaces proved in StacksFrontier/AlgebraicGeometry/Spaces/ReducedClosedSubspaceDefiningIdeal.lean: the defining ideals of the subspaces on two disjoint closed sets are comaximal on every affine chart, and the defining ideal sheaves of the subspaces on Z₀ and on Z₁ meet in that of the subspace on Z₀ ∪ Z₁. The passage from the resulting ideal memberships to the point-set conclusion is AlgebraicGeometry.Space.subset_compl_sectionSupport_of_forall_mem_definingIdealAt.

The situation is one at the module universe of the structure sheaf — see the implementation notes — because that is the form in which the lifting statement AlgebraicGeometry.Space.CohomologyVanishingSituation.surjective_sectionsMap_of_epi is available.

theorem exists_subset_compl_sectionSupport_of_disjoint
    {Z₀ Z₁ : Set (points T'.site T'.base T'.containsBase T'.space.1)}
    (hZ₀ : IsClosed Z₀) (hZ₁ : IsClosed Z₁) (hdisj : Disjoint Z₀ Z₁) :
    ∃ a : _root_.AlgebraicGeometry.Space.globalFunctions
        T'.site T'.base T'.containsBase T'.space.1,
      Z₀ ⊆ (_root_.AlgebraicGeometry.Space.sectionSupport
          T'.site T'.base T'.containsBase T'.space.1 a)ᶜ ∧
        Z₁ ⊆ (_root_.AlgebraicGeometry.Space.sectionSupport
          T'.site T'.base T'.containsBase T'.space.1 (a - 1))ᶜ

Tag 07V4, a lemma

Tag 07V4 in the Stacks Project.

AlgebraicGeometry.Space.CohomologyVanishingSituation.pointsToScheme_pointsMap_toSpecGlobalFunctions_ne_of_isClosed_of_ne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohomologyVanishingClosedPoints.lean, line 190. The attribute's comment: “the final step of the source proof only: in Situation 07UY the morphism p : X -> Spec A separates the closed points of |X|, two distinct closed points of |X| having distinct images. Universal injectivity of p, which is the assertion of the tag, is NOT proved by this declaration, and neither is injectivity of p on all of |X|; see universallyInjective_toSpecGlobalFunctions in this same file, which does state universal injectivity and carries the two steps that are missing. The source reaches universal injectivity from this step by three reductions, none of them available in this development. Clause (2) of Stacks 07V0 reduces to the case of a field A, but its library form -- isAffineHom_of_isPullback_toSpecGlobalFunctions -- carries the affineness assertion only and not the computation Gamma(X', O_X') = A' that the reduction needs. Stacks 0488 then replaces the field by a large algebraically closed extension and Stacks 07U5 makes the resulting field-valued points closed points of |X|, but the library's 07U5 -- isClosed_singleton_class_of_isAlgebraic_residueField -- requires the field of the point to be algebraic over the residue field at a closed point of the base, which is exactly what the first reduction would have arranged. And the source's passage from one point of |X| to one field-valued point of X is left implicit there. IsTerminal T'.base, the affine object V and the isomorphism e are inherited from the signature of toSpecGlobalFunctions, as for the neighbouring Stacks 07V5”.

The canonical morphism to Spec A separates the closed points of |X|. In the situation of Stacks 07UY, two distinct closed points of |X| have distinct images in Spec A under p : X ⟶ Spec A, where Spec A is presented by an affine object V of the site through a ring isomorphism Γ(V, 𝒪_V) ≅ A = Γ(X, 𝒪_X).

Stacks 07V1 supplies a ∈ A vanishing at the first point and taking the value 1 at the second; if the two images agreed, that point of Spec A would lie in neither the nonvanishing locus of a nor that of a - 1, which no point of a scheme does.

theorem pointsToScheme_pointsMap_toSpecGlobalFunctions_ne_of_isClosed_of_ne
    {x y : points T'.site T'.base T'.containsBase T'.space.1}
    (hx : IsClosed ({x} : Set (points T'.site T'.base T'.containsBase T'.space.1)))
    (hy : IsClosed ({y} : Set (points T'.site T'.base T'.containsBase T'.space.1)))
    (hxy : x ≠ y) :
    pointsToScheme T'.site T'.base T'.containsBase V
        (pointsMap T'.site T'.base T'.containsBase T'.space.1
          (toSpecGlobalFunctions T' hterminal V e).hom x) ≠
      pointsToScheme T'.site T'.base T'.containsBase V
        (pointsMap T'.site T'.base T'.containsBase T'.space.1
          (toSpecGlobalFunctions T' hterminal V e).hom y)

AlgebraicGeometry.Space.CohomologyVanishingSituation.universallyInjective_toSpecGlobalFunctionsOverIntegers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohomologyVanishingUniversallyInjective.lean, line 132.

Stacks 07V4. In the situation of Stacks 07UY, over an arbitrary base scheme S, the canonical morphism p : X ⟶ Spec A is universally injective. As in the source, p is the morphism of Stacks 05Z1 formed after regarding X as an algebraic space over Spec ℤ, and Spec A is presented by an affine object V of the site through a ring isomorphism Γ(V, 𝒪_V) ≅ A = Γ(X, 𝒪_X).

The view of X over Spec ℤ has the same small étale ringed site, hence the same global functions and right exact global sections, and it is quasi-compact and quasi-separated; the statement is then AlgebraicGeometry.Space.universallyInjective_of_surjective_pullbackToGlobalFunctions.

theorem universallyInjective_toSpecGlobalFunctionsOverIntegers :
    _root_.AlgebraicGeometry.Space.UniversallyInjective T.site (⊤_ Scheme.{u}) T.containsTerminal
      (toSpecGlobalFunctionsOverIntegers T V e).hom

Tag 07V5, a lemma

Tag 07V5 in the Stacks Project.

AlgebraicGeometry.Space.CohomologyVanishingSituation.isSeparated_toSpecGlobalFunctions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohomologyVanishingSeparatedMorphism.lean, line 187. The attribute's comment: “two inputs are carried as named hypotheses -- h09YB, clause (1) of Stacks 09YB, and h07V0, clause (1) of Stacks 07V0 for a scheme of the site affine over X with its first cohomology read in the Zariski topology of that scheme. IsTerminal T.base is inherited from the signature of toSpecGlobalFunctions. See this file's implementation notes”.

Stacks 07V5. In the situation of Stacks 07UY, the canonical morphism p : X ⟶ Spec Γ(X, 𝒪_X) is separated, Spec Γ(X, 𝒪_X) being presented by an affine object V of the site through a ring isomorphism Γ(V, 𝒪_V) ≅ Γ(X, 𝒪_X).

theorem isSeparated_toSpecGlobalFunctions
    (h09YB : ExistsIntegralSurjectiveSchemeCover T.site T.base T.containsBase T.space.1)
    (h07V0 : SchemeAffineOverFirstZariskiCohomologyVanishing T.site T.base T.containsBase
      T.space.1) :
    IsSeparated T.site T.base T.containsBase
      (toSpecGlobalFunctions T hterminal V e).hom

AlgebraicGeometry.Space.CohomologyVanishingSituation.isSeparated_toSpecGlobalFunctionsOverIntegers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SeparatedOverGlobalFunctions.lean, line 116.

Stacks 07V5. In the situation of Stacks 07UY, over an arbitrary base scheme S, the canonical morphism p : X ⟶ Spec A is separated. As in the source, p is the morphism of Stacks 05Z1 formed after regarding X as an algebraic space over Spec ℤ, and Spec A is presented by an affine object V of the site through a ring isomorphism Γ(V, 𝒪_V) ≅ A = Γ(X, 𝒪_X).

The view of X over Spec ℤ has right exact global sections on quasi-coherent modules and is quasi-compact and quasi-separated, and every global function on it is pulled back along p; the statement is then AlgebraicGeometry.Space.isSeparated_of_surjective_pullbackToGlobalFunctions.

theorem isSeparated_toSpecGlobalFunctionsOverIntegers :
    IsSeparated T.site (⊤_ Scheme.{u}) T.containsTerminal
      (toSpecGlobalFunctionsOverIntegers T V e).hom

Tag 07V6, a proposition

Tag 07V6 in the Stacks Project.

AlgebraicGeometry.Space.CohomologyVanishingSituation.isAffineSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AffinenessCriteria.lean, line 63. The attribute's comment: “more precisely: an algebraic space as in Situation 07UY is an affine scheme”.

Stacks 07V6, more precisely. An algebraic space in the situation of Stacks 07UY is an affine scheme: it is represented by an object of the site over the base whose underlying scheme is affine.

theorem isAffineSpace (T : CohomologyVanishingSituation.{u, u}) :
    IsAffineSpace T.site T.base T.containsBase T.space.1

Declarations registered for the tag:

AlgebraicGeometry.Space.isAffineSpace_iff_forall_isZero_rightDerived, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/AffinenessCriteria.lean, line 48 (StacksFrontier): “first sentence: a quasi-compact and quasi-separated algebraic space is affine iff the higher cohomology of its quasi-coherent modules vanishes”.

Tag 0D2V, a lemma

Tag 0D2V in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.Space.isAffineSpace_of_forall_isCoherent_isZero_rightDerived_one, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/AffinenessCriteria.lean, line 52 (StacksFrontier).

Tag 0D2W, a lemma

Tag 0D2W in the Stacks Project.

AlgebraicGeometry.Space.exists_isAmple_of_forall_isCoherent_isZero_rightDerived_one_twistStep, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohomologicalAmplenessCriterion.lean, line 201.

Stacks 0D2W. Let S be a scheme, X a Noetherian algebraic space over S and 𝓛 an invertible 𝒪_X-module. If every coherent 𝒪_X-module 𝓕 has some n ≥ 1 with H¹(X, 𝓕 ⊗ 𝓛^{⊗ n}) = 0, then X is a scheme and 𝓛 is ample on it: there are an object U of the site and an isomorphism yoneda.obj U ≅ X for which the restriction of 𝓛 to the scheme underlying U is an invertible and ample module. See the module docstring.

theorem exists_isAmple_of_forall_isCoherent_isZero_rightDerived_one_twistStep
    (hZ : B.Contains (⊤_ Scheme.{u})) (X : AlgebraicSpaces B S hS)
    (hN : IsNoetherian B S hS hZ X.1) (L : Modules.{u, u} B S hS X.1 X.2)
    [hL : Stacks.SheafOfModules.IsInvertible (structurePresheaf B S hS X.1)
      (Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS X.1 X.2).O).property L]
    (h : have := enoughInjectives_modules B S hS X.1 X.2
      ∀ F : Modules.{u, u} B S hS X.1 X.2, IsCoherent B S hS X.1 X.2 F →
        ∃ n : ℕ, 1 ≤ n ∧ IsZero (((globalSectionsFunctor.{u + 1, u, u, u}
          (Stacks.SheafOfModules.Tensor.ringSheaf
            (smallEtaleRingedSite B S hS X.1 X.2).O)).rightDerived 1).obj
            (twistStep B S hS X.1 X.2 L n F))) :
    ∃ (U : BigFppfOver B S hS) (eX : yoneda.obj U ≅ X.1)
      (_ : Stacks.Ample.IsInvertibleModule ((BigFppfOver.toScheme B S hS).obj U)
        (baseChangeModule B S hS L U eX.hom)),
      Stacks.Ample.IsAmple ((BigFppfOver.toScheme B S hS).obj U)
        (baseChangeModule B S hS L U eX.hom)

Sources

LeanAlgebraicGeometry.Space.CohomologyVanishingSituation · AlgebraicGeometry.Space.CohomologyVanishingSituation.isIso_unit_tensorSheaf · AlgebraicGeometry.Space.CohomologyVanishingSituation.globalSectionsTensorLinearEquiv · Stacks.Cohomology.SiteModules.sectionTensorFreeIso · Stacks.Cohomology.SiteModules.sectionTensorSheafAdjunction · Stacks.Cohomology.SiteModules.isIso_sectionTensorSheafUnit_free · Stacks.Cohomology.SiteModules.isQuasicoherentOnSite_sectionTensor · AlgebraicGeometry.Space.CohomologyVanishingSituation.isZero_rightDerived_one_globalSectionsFunctor_of_isAffineHom

Section69.17 Finite morphisms and affines #

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

Tag 0GF7, a lemma

Tag 0GF7 in the Stacks Project.

AlgebraicGeometry.Space.isCoherent_and_supportOfSheaf_eq_univ_modulePushforward_structureSheaf_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteDirectImageChartCartesian.lean, line 259. The attribute's comment: “the whole statement: for f finite and surjective with X locally Noetherian and i : Z -> X a closed immersion, the direct image f'_* O_{Z'} along the induced morphism of the inverse image is a coherent O_Z-module, and its support is all of Z”.

Let S be a scheme and let f : Y ⟶ X be a morphism of algebraic spaces over S which is finite and surjective, with X locally Noetherian. Let i : Z ⟶ X be a closed immersion, let i' : Z' ⟶ Y be the inverse image of Z, and let f' : Z' ⟶ Z be the induced morphism. Then 𝒢 = f'_*𝒪_{Z'} is a coherent 𝒪_Z-module whose support is all of Z.

theorem isCoherent_and_supportOfSheaf_eq_univ_modulePushforward_structureSheaf_preimage
    {Z Z' : AlgebraicSpaces B S hS} (f : Y ⟶ X) (i : Z ⟶ X) {i' : Z' ⟶ Y} {f' : Z' ⟶ Z}
    (sq : IsPullback i' f' f i) (hf : IsFinite B S hS f.hom)
    (hsurj : IsSurjective B S hS f.hom)
    (hX : HasEtaleLocalProperty B S hS X.1 (fun T : Scheme.{u} ↦ IsLocallyNoetherian T))
    (hi : IsClosedImmersion B S hS i.hom) :
    IsCoherent B S hS Z.1 Z.2 ((modulePushforward B S hS f').obj
        (SheafOfModules.unit (structureRingSheaf B S hS Z'))) ∧
      supportOfSheaf B S hS Z.1 ((SheafOfModules.toSheaf _).obj
        ((modulePushforward B S hS f').obj
          (SheafOfModules.unit (structureRingSheaf B S hS Z')))) = Set.univ

AlgebraicGeometry.Space.isCoherent_modulePushforward_structureSheaf_preimage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePreimageStructureSheaf.lean, line 241. The attribute's comment: “coherence of the direct image, granted the chart case hchart of Stacks 03DW which Tag 07UH already carries”.

The coherence assertion of Stacks 0GF7, granted the chart case hchart. Let f : Y ⟶ X be a finite morphism of algebraic spaces over S with X locally Noetherian, let i : Z ⟶ X be a closed immersion, and let f' : Z' ⟶ Z be the base change of f along i. Then 𝒢 = f'_*𝒪_{Z'} is a coherent 𝒪_Z-module.

Z is locally Noetherian by Stacks 06ED and 04ZK, f' is finite by Stacks 03ZS, Z' is locally Noetherian for the same reason as Z, and 𝒪_{Z'} is then coherent by Stacks 07UB; so this is AlgebraicGeometry.Space.isCoherent_modulePushforward_of_isFinite, whose hypothesis hchart is the étale-site form of Stacks 01Y6, that is Stacks 03DW, which this development does not carry. Surjectivity of f is not used.

theorem isCoherent_modulePushforward_structureSheaf_preimage (f : Y ⟶ X) (i : Z ⟶ X)
    {i' : Z' ⟶ Y} {f' : Z' ⟶ Z} (sq : IsPullback i' f' f i)
    (hf : IsFinite B S hS f.hom)
    (hX : HasEtaleLocalProperty B S hS X.1 (fun T : Scheme.{u} ↦ IsLocallyNoetherian T))
    (hi : IsClosedImmersion B S hS i.hom)
    (V : SmallEtale B S hS Z.1) (hsurj : IsSurjective B S hS V.1.hom)
    (hchart : IsFinite B S hS (chartBaseChangeProjection B S hS f' V).hom →
      HasEtaleLocalProperty B S hS
        ((SpacesEtale.toSpaces B S hS Z).obj ((comparisonFunctor B S hS Z).obj V)).1
        (fun T : Scheme.{u} ↦ IsLocallyNoetherian T) →
      IsCoherent B S hS Z'.1 Z'.2 (SheafOfModules.unit (structureRingSheaf B S hS Z')) →
      ((chartLocalizedModulePushforward B S hS f' V).obj
        ((moduleChartBaseChangeRestriction B S hS f' V).obj
          (SheafOfModules.unit (structureRingSheaf B S hS Z')))).IsCoherentOnSite) :
    IsCoherent B S hS Z.1 Z.2 ((modulePushforward B S hS f').obj
      (SheafOfModules.unit (structureRingSheaf B S hS Z')))

AlgebraicGeometry.Space.supportOfSheaf_modulePushforward_structureSheaf_preimage_eq_univ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePreimageStructureSheaf.lean, line 280. The attribute's comment: “the support of the direct image is all of Z”.

The support assertion of Stacks 0GF7. Let f : Y ⟶ X be a surjective morphism of algebraic spaces over S, let i : Z ⟶ X be any morphism and let f' : Z' ⟶ Z be the base change of f along i. Then the support of 𝒢 = f'_*𝒪_{Z'} is all of Z.

Surjectivity is stable under base change by Stacks 03MH, so this is AlgebraicGeometry.Space.supportOfSheaf_modulePushforward_structureSheaf_eq_univ. Neither the finiteness of f, nor the local Noetherianity of X, nor the closedness of the immersion i is used.

theorem supportOfSheaf_modulePushforward_structureSheaf_preimage_eq_univ (f : Y ⟶ X) (i : Z ⟶ X)
    {i' : Z' ⟶ Y} {f' : Z' ⟶ Z} (sq : IsPullback i' f' f i)
    (hf : IsSurjective B S hS f.hom) :
    supportOfSheaf B S hS Z.1 ((SheafOfModules.toSheaf _).obj
        ((modulePushforward B S hS f').obj
          (SheafOfModules.unit (structureRingSheaf B S hS Z')))) = Set.univ

AlgebraicGeometry.Space.isCoherent_modulePushforward_structureSheaf_preimage_of_isLocallyNoetherian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FinitePreimageStructureSheafCoherent.lean, line 53. The attribute's comment: “coherence of the direct image”.

The coherence assertion of Stacks 0GF7. Let f : Y ⟶ X be a finite morphism of algebraic spaces over S with X locally Noetherian, let i : Z ⟶ X be a closed immersion, and let f' : Z' ⟶ Z be the base change of f along i. Then 𝒢 = f'_*𝒪_{Z'} is a coherent 𝒪_Z-module.

Z is locally Noetherian by Stacks 06ED and 04ZK, f' is finite by Stacks 03ZS, Z' is locally Noetherian for the same reason as Z, and 𝒪_{Z'} is then coherent by Stacks 07UB; so this is Stacks 07UH, AlgebraicGeometry.Space.isCoherent_modulePushforward_of_isFinite'. Surjectivity of f is not used.

theorem isCoherent_modulePushforward_structureSheaf_preimage_of_isLocallyNoetherian (f : Y ⟶ X)
    (i : Z ⟶ X) {i' : Z' ⟶ Y} {f' : Z' ⟶ Z} (sq : IsPullback i' f' f i)
    (hf : IsFinite B S hS f.hom)
    (hX : HasEtaleLocalProperty B S hS X.1 (fun T : Scheme.{u} ↦ IsLocallyNoetherian T))
    (hi : IsClosedImmersion B S hS i.hom) :
    IsCoherent B S hS Z.1 Z.2 ((modulePushforward B S hS f').obj
      (SheafOfModules.unit (structureRingSheaf B S hS Z')))

Tag 0GF8, a lemma

Tag 0GF8 in the Stacks Project.

AlgebraicGeometry.Space.idealSmul_pushforward_eq_of_isQuasicoherentOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IdealPushforwardAffineComparison.lean, line 255.

Stacks 0GF8. Let S be a scheme, let f : Y ⟶ X be a morphism of algebraic spaces over S, let F be a quasi-coherent sheaf on Y and let I be a quasi-coherent sheaf of ideals on X. If f is affine then

I · f_*F = f_*((f⁻¹I) · F)

as subsheaves of f_*F.

This is AlgebraicGeometry.Space.idealSmul_pushforward_eq with quasi-coherence, rather than the equivalent cartesian condition on affine charts, as the hypothesis of the source.

theorem idealSmul_pushforward_eq_of_isQuasicoherentOnSite
    (hI : I.toSheafOfModules.IsQuasicoherentOnSite) (hF : F.IsQuasicoherentOnSite) :
    Stacks.Sites.idealSmul (O := structureSheaf B S hS X.1 X.2)
        I (⊤ : ((smallBaseChangeModulePushforward B S hS f
          (relativelyRepresentable_hom_of_isAffineHom B S hS f haff)).obj F).Submodule) =
      pushforwardSubmodule B S hS f
        (relativelyRepresentable_hom_of_isAffineHom B S hS f haff) F
        (Stacks.Sites.idealSmul (O := structureSheaf B S hS Y.1 Y.2)
          (pullbackIdealSubsheaf B S hS f
            (relativelyRepresentable_hom_of_isAffineHom B S hS f haff) I) (⊤ : F.Submodule))

Tag 07VP, a lemma

Tag 07VP in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.Space.isAffineSpace_of_isFinite_of_isSurjective, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/AffinenessCriteria.lean, line 55 (StacksFrontier).

Sources

LeanAlgebraicGeometry.Space.isCoherent_and_supportOfSheaf_eq_univ_modulePushforward_structureSheaf_preimage · AlgebraicGeometry.Space.isCoherent_modulePushforward_structureSheaf_preimage · AlgebraicGeometry.Space.supportOfSheaf_modulePushforward_structureSheaf_preimage_eq_univ · AlgebraicGeometry.Space.isCoherent_modulePushforward_structureSheaf_preimage_of_isLocallyNoetherian · AlgebraicGeometry.Space.idealSmul_pushforward_eq_of_isQuasicoherentOnSite · AlgebraicGeometry.Space.isAffineSpace_of_isFinite_of_isSurjective

Section69.18 A weak version of Chow's lemma #

Section 69.18 of the Stacks Project, Tag 089I. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 089J, a lemma

Tag 089J in the Stacks Project.

AlgebraicGeometry.Space.hasChowSchemeCover_of_isSeparated_isFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ChowLemma/Induction.lean, line 288.

Chow's lemma for algebraic spaces, [Stacks, Tag 089J].

Let A be a ring whose spectrum lies in the chosen big fppf site, and let X be an algebraic space over Spec A whose structure morphism is separated and of finite type. Then there is an object X' of the site — a scheme over Spec A — and a proper surjective morphism from the presheaf it represents to X, such that the structure morphism of X' to Spec A is H-quasi-projective.

The morphism f quantified over is the structure morphism of X and nothing else: its target is the presheaf represented by the base, which is terminal by AlgebraicGeometry.Space.isTerminal_yoneda_obj_base.

The proof is Stacks 089J's. An affine surjective étale chart exists by Stacks 03H6; a separated algebraic space over an affine base is reasonable by Stacks 03JX, so the fibre degrees of that chart are bounded, by the degree stratification of Stacks 07S8; and AlgebraicGeometry.Space.hasChowSchemeCover_of_chart_fibre_le performs the induction on that bound.

theorem hasChowSchemeCover_of_isSeparated_isFiniteType
    (B : BigFppfSite.{u}) (A : CommRingCat.{u}) (hA : B.Contains (Spec A))
    (X : (BigFppfOver B (Spec A) hA)ᵒᵖ ⥤ Type u) (hX : IsAlgebraicSpace B (Spec A) hA X)
    (f : X ⟶ yoneda.obj (Over.mk (𝟙 (B.obj hA))))
    (hsep : IsSeparated B (Spec A) hA f) (hft : IsFiniteType B (Spec A) hA f) :
    HasChowSchemeCover B (Spec A) hA X

Sources

LeanAlgebraicGeometry.Space.hasChowSchemeCover_of_isSeparated_isFiniteType

Section69.19 Noetherian valuative criterion #

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

Tag 0ARJ, a lemma

Tag 0ARJ in the Stacks Project.

AlgebraicGeometry.Space.isSeparated_of_isQuasiSeparated_of_discreteValuativeUniqueness, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NoetherianValuativeSeparated.lean, line 183.

Stacks 0ARJ. Let f : X ⟶ Y be a morphism of algebraic spaces over S with Y locally Noetherian. If f is locally of finite type and quasi-separated, and every valuative square for f whose valuation ring is a discrete valuation ring admits at most one dotted arrow, then f is separated.

theorem isSeparated_of_isQuasiSeparated_of_discreteValuativeUniqueness
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (hX : IsAlgebraicSpace B S hS X)
    (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hNoeth : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} ↦ IsLocallyNoetherian T))
    (hft : IsLocallyOfFiniteType B S hS f) (hqs : IsQuasiSeparated B S hS f)
    (hu : ∀ q : ValuativeSquare f, IsDiscreteValuationRing q.R → Subsingleton q.Lift) :
    IsSeparated B S hS f

Tag 0ARK, a lemma

Tag 0ARK in the Stacks Project.

AlgebraicGeometry.Space.isProper_of_isQuasiSeparated_of_discreteValuativeCriterion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NoetherianValuativeProper.lean, line 276.

Stacks 0ARK. Let f : X ⟶ Y be a morphism of algebraic spaces over S with Y locally Noetherian. If f is of finite type and quasi-separated, and every valuative square for f whose valuation ring is a discrete valuation ring has exactly one dotted arrow, then f is proper.

theorem isProper_of_isQuasiSeparated_of_discreteValuativeCriterion
    (hX : IsAlgebraicSpace B S hS X) (hY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (hNoeth : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} ↦ IsLocallyNoetherian T))
    (hft : IsFiniteType B S hS f) (hqs : IsQuasiSeparated B S hS f)
    (hlift : ∀ q : ValuativeSquare f, IsDiscreteValuationRing q.R →
      Nonempty q.Lift ∧ Subsingleton q.Lift) :
    IsProper B S hS f

Tag 0ARL, a remark

Tag 0ARL in the Stacks Project.

AlgebraicGeometry.Space.isSeparated_iff_discreteValuativeUniqueness_of_isCofinal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NoetherianValuativeComplete.lean, line 177. The attribute's comment: “Lemma 69.19.1 (0ARJ) for any class of discrete valuation rings in which every discrete valuation ring has an extension”.

Let f : X ⟶ Y be a morphism of algebraic spaces over S with Y locally Noetherian, and assume f is locally of finite type and quasi-separated. Let P be a class of discrete valuation rings such that every discrete valuation ring has an extension in the class. If every valuative square for f whose valuation ring is a discrete valuation ring in the class admits at most one dotted arrow, then f is separated; and conversely.

theorem isSeparated_iff_discreteValuativeUniqueness_of_isCofinal
    {P : ∀ (A : Type u) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A], Prop}
    (cofinal : IsCofinalDiscreteValuationRingClass B P)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (algX : IsAlgebraicSpace B S hS X)
    (algY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (noethY : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} ↦ IsLocallyNoetherian T))
    (finf : IsLocallyOfFiniteType B S hS f) (qsepf : IsQuasiSeparated B S hS f) :
    IsSeparated B S hS f ↔
      ∀ q : ValuativeSquare f, ∀ _ : IsDiscreteValuationRing q.R, P q.R → Subsingleton q.Lift

AlgebraicGeometry.Space.isProper_iff_discreteValuativeCriterion_of_isCofinal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NoetherianValuativeComplete.lean, line 202. The attribute's comment: “Lemma 69.19.2 (0ARK) for any class of discrete valuation rings in which every discrete valuation ring has an extension”.

Let f : X ⟶ Y be a morphism of algebraic spaces over S with Y locally Noetherian, and assume f is of finite type and quasi-separated. Let P be a class of discrete valuation rings such that every discrete valuation ring has an extension in the class. If for every valuative square for f whose valuation ring A is a discrete valuation ring in the class there is an extension A ⊂ A' of discrete valuation rings in the class, inducing an extension of fraction fields, over which the square has exactly one dotted arrow Spec A' ⟶ X, then f is proper; and conversely.

theorem isProper_iff_discreteValuativeCriterion_of_isCofinal
    {P : ∀ (A : Type u) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A], Prop}
    (cofinal : IsCofinalDiscreteValuationRingClass B P)
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (algX : IsAlgebraicSpace B S hS X)
    (algY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (noethY : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} ↦ IsLocallyNoetherian T))
    (finf : IsFiniteType B S hS f) (qsepf : IsQuasiSeparated B S hS f) :
    IsProper B S hS f ↔ ∀ q : ValuativeSquare f, ∀ _ : IsDiscreteValuationRing q.R, P q.R →
      ∃ e : q.DominatingExtension, ∃ _ : IsDiscreteValuationRing e.square.R, P e.square.R ∧
        Nonempty e.square.Lift ∧ Subsingleton e.square.Lift

AlgebraicGeometry.Space.isSeparated_iff_completeDiscreteValuativeUniqueness, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NoetherianValuativeComplete.lean, line 235. The attribute's comment: “Lemma 69.19.1 (0ARJ) with complete discrete valuation rings”.

Let f : X ⟶ Y be a morphism of algebraic spaces over S with Y locally Noetherian, and assume f is locally of finite type and quasi-separated. If every valuative square for f whose valuation ring is a complete discrete valuation ring admits at most one dotted arrow, then f is separated; and conversely.

theorem isSeparated_iff_completeDiscreteValuativeUniqueness
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (algX : IsAlgebraicSpace B S hS X)
    (algY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (noethY : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} ↦ IsLocallyNoetherian T))
    (finf : IsLocallyOfFiniteType B S hS f) (qsepf : IsQuasiSeparated B S hS f) :
    IsSeparated B S hS f ↔ ∀ q : ValuativeSquare f, IsDiscreteValuationRing q.R →
      IsAdicComplete (IsLocalRing.maximalIdeal q.R) q.R → Subsingleton q.Lift

AlgebraicGeometry.Space.isProper_iff_completeDiscreteValuativeCriterion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NoetherianValuativeComplete.lean, line 252. The attribute's comment: “Lemma 69.19.2 (0ARK) with complete discrete valuation rings”.

Let f : X ⟶ Y be a morphism of algebraic spaces over S with Y locally Noetherian, and assume f is of finite type and quasi-separated. If for every valuative square for f whose valuation ring A is a complete discrete valuation ring, with fraction field K, there is an extension A ⊂ A' of complete discrete valuation rings inducing an extension K ⊂ K' of fraction fields over which the square has exactly one dotted arrow Spec A' ⟶ X, then f is proper; and conversely.

theorem isProper_iff_completeDiscreteValuativeCriterion
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (algX : IsAlgebraicSpace B S hS X)
    (algY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (noethY : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} ↦ IsLocallyNoetherian T))
    (finf : IsFiniteType B S hS f) (qsepf : IsQuasiSeparated B S hS f) :
    IsProper B S hS f ↔ ∀ q : ValuativeSquare f, IsDiscreteValuationRing q.R →
      IsAdicComplete (IsLocalRing.maximalIdeal q.R) q.R →
      ∃ e : q.DominatingExtension, IsDiscreteValuationRing e.square.R ∧
        IsAdicComplete (IsLocalRing.maximalIdeal e.square.R) e.square.R ∧
        Nonempty e.square.Lift ∧ Subsingleton e.square.Lift

AlgebraicGeometry.Space.isSeparated_iff_completeAlgClosedDiscreteValuativeUniqueness, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NoetherianValuativeComplete.lean, line 273. The attribute's comment: “Lemma 69.19.1 (0ARJ) with complete discrete valuation rings with algebraically closed residue field”.

Let f : X ⟶ Y be a morphism of algebraic spaces over S with Y locally Noetherian, and assume f is locally of finite type and quasi-separated. If every valuative square for f whose valuation ring is a complete discrete valuation ring with algebraically closed residue field admits at most one dotted arrow, then f is separated; and conversely.

theorem isSeparated_iff_completeAlgClosedDiscreteValuativeUniqueness
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (algX : IsAlgebraicSpace B S hS X)
    (algY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (noethY : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} ↦ IsLocallyNoetherian T))
    (finf : IsLocallyOfFiniteType B S hS f) (qsepf : IsQuasiSeparated B S hS f) :
    IsSeparated B S hS f ↔ ∀ q : ValuativeSquare f, IsDiscreteValuationRing q.R →
      IsAdicComplete (IsLocalRing.maximalIdeal q.R) q.R →
      IsAlgClosed (IsLocalRing.ResidueField q.R) → Subsingleton q.Lift

AlgebraicGeometry.Space.isProper_iff_completeAlgClosedDiscreteValuativeCriterion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/NoetherianValuativeComplete.lean, line 293. The attribute's comment: “Lemma 69.19.2 (0ARK) with complete discrete valuation rings with algebraically closed residue field”.

Let f : X ⟶ Y be a morphism of algebraic spaces over S with Y locally Noetherian, and assume f is of finite type and quasi-separated. If for every valuative square for f whose valuation ring A is a complete discrete valuation ring with algebraically closed residue field there is an extension A ⊂ A' of such rings, inducing an extension of fraction fields, over which the square has exactly one dotted arrow Spec A' ⟶ X, then f is proper; and conversely.

theorem isProper_iff_completeAlgClosedDiscreteValuativeCriterion
    {X Y : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u} (algX : IsAlgebraicSpace B S hS X)
    (algY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (noethY : HasEtaleLocalProperty B S hS Y (fun T : Scheme.{u} ↦ IsLocallyNoetherian T))
    (finf : IsFiniteType B S hS f) (qsepf : IsQuasiSeparated B S hS f) :
    IsProper B S hS f ↔ ∀ q : ValuativeSquare f, IsDiscreteValuationRing q.R →
      IsAdicComplete (IsLocalRing.maximalIdeal q.R) q.R →
      IsAlgClosed (IsLocalRing.ResidueField q.R) →
      ∃ e : q.DominatingExtension, IsDiscreteValuationRing e.square.R ∧
        IsAdicComplete (IsLocalRing.maximalIdeal e.square.R) e.square.R ∧
        IsAlgClosed (IsLocalRing.ResidueField e.square.R) ∧
        Nonempty e.square.Lift ∧ Subsingleton e.square.Lift

Sources

LeanAlgebraicGeometry.Space.isSeparated_of_isQuasiSeparated_of_discreteValuativeUniqueness · AlgebraicGeometry.Space.isProper_of_isQuasiSeparated_of_discreteValuativeCriterion · AlgebraicGeometry.Space.isSeparated_iff_discreteValuativeUniqueness_of_isCofinal · AlgebraicGeometry.Space.isProper_iff_discreteValuativeCriterion_of_isCofinal · AlgebraicGeometry.Space.isSeparated_iff_completeDiscreteValuativeUniqueness · AlgebraicGeometry.Space.isProper_iff_completeDiscreteValuativeCriterion · AlgebraicGeometry.Space.isSeparated_iff_completeAlgClosedDiscreteValuativeUniqueness · AlgebraicGeometry.Space.isProper_iff_completeAlgClosedDiscreteValuativeCriterion

Section69.20 Higher direct images of coherent sheaves #

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

Tag 08AQ, a lemma

Tag 08AQ in the Stacks Project.

AlgebraicGeometry.Space.ProjectiveSpaceImmersion.twist, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProjectiveTwistHigherDirectImageVanishing.lean, line 221. The attribute's comment: “the twist L = i^* O_{P^n_Y}(1) of the statement”.

The twist L = i^* O_{P^n_Y}(1) of Stacks 08AQ: the inverse image of the hyperplane sheaf of P^n_S along X ⟶ P^n_Y ⟶ P^n_S.

noncomputable def twist (D : ProjectiveSpaceImmersion B S hS n hP X Y) :
    Modules.{u, u} B S hS X.1 X.2

AlgebraicGeometry.Space.exists_isZero_rightDerived_modulePushforward_tensor_twist, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProjectiveTwistHigherDirectImageVanishing.lean, line 276. The attribute's comment: “the étale-local reduction of the source's proof, by Stacks 071Z, with representability of the composite proved; the scheme case, where the source cites Stacks 02O1, is carried as the hypothesis h02O1 and is not proved — note that h02O1 is this same eventual vanishing after base change to an étale scheme chart of Y, so it is the source's reduction target rather than side-work, and discharging it needs both the conditional repository form of Stacks 02O1 and the étale-versus-Zariski comparison Stacks 03DW”.

Stacks 08AQ, with the scheme case carried as h02O1.

Let i : X ⟶ P^n_Y be a closed immersion of algebraic spaces over S with Y Noetherian, let f : X ⟶ Y be the composite with the projection and let L = i^* O_{P^n_Y}(1). For a coherent 𝒪_X-module F there is a d₀ such that

R^p f_*(F ⊗ L^{⊗ d}) = 0 for all d ≥ d₀ and all p > 0.

The source's proof is the étale-local reduction on Y, and that is what is proved: Equation 69.3.0.1 (Stacks 071Z) identifies the restriction of R^p f_* to an étale scheme chart of Y with the corresponding higher direct image of the base change, and a module on the small étale site of Y vanishes as soon as all those restrictions do. Representability of f, which Stacks 071Z needs, is supplied by AlgebraicGeometry.Space.ProjectiveSpaceImmersion.relativelyRepresentable_hom. What remains is the conclusion over a scheme chart, which is where the source cites Stacks 02O1; it is carried as h02O1 and is not proved. Noetherianity of Y and coherence of F are the source's hypotheses and are what would discharge h02O1; the reduction itself uses neither.

theorem exists_isZero_rightDerived_modulePushforward_tensor_twist
    (hZ : B.Contains (⊤_ Scheme.{u})) (n : ℕ)
    (hP : B.Contains (projectiveSpaceOver n S)) {X Y : AlgebraicSpaces B S hS}
    (D : ProjectiveSpaceImmersion B S hS n hP X Y)
    (hY : IsNoetherian B S hS hZ Y.1) (F : Modules.{u, u} B S hS X.1 X.2)
    (hF : IsCoherent B S hS X.1 X.2 F)
    (h02O1 : ChartwiseEventualTwistVanishing B S hS D.hom D.relativelyRepresentable_hom F
      D.twist) :
    have := hasInjectiveResolutions_modules B S hS X.1 X.2
    ∃ d₀ : ℕ, ∀ d : ℕ, d₀ ≤ d → ∀ p : ℕ, 0 < p →
      IsZero (((modulePushforward B S hS D.hom).rightDerived p).obj
        (F ⊗ tensorPow B S hS D.twist d))

AlgebraicGeometry.Space.exists_twistBound_isZero_rightDerived_modulePushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProjectiveTwistHigherDirectImageVanishingNoetherian.lean, line 446.

Stacks 08AQ. Let i : X ⟶ P^n_Y be a closed immersion of algebraic spaces over S with Y Noetherian, let f : X ⟶ Y be the composite with the projection and let L = i^* O_{P^n_Y}(1). For a coherent 𝒪_X-module F there is a d₀ such that

R^p f_*(F ⊗ L^{⊗ d}) = 0 for all d ≥ d₀ and all p > 0.

theorem exists_twistBound_isZero_rightDerived_modulePushforward
    (hZ : B.Contains (⊤_ Scheme.{u})) (n : ℕ)
    (hP : B.Contains (projectiveSpaceOver n S)) {X Y : AlgebraicSpaces B S hS}
    (D : ProjectiveSpaceImmersion B S hS n hP X Y)
    (hY : IsNoetherian B S hS hZ Y.1) (F : Modules.{u, u} B S hS X.1 X.2)
    (hF : IsCoherent B S hS X.1 X.2 F) :
    have := hasInjectiveResolutions_modules B S hS X.1 X.2
    ∃ d₀ : ℕ, ∀ d : ℕ, d₀ ≤ d → ∀ p : ℕ, 0 < p →
      IsZero (((modulePushforward B S hS D.hom).rightDerived p).obj
        (F ⊗ tensorPow B S hS D.twist d))

Tag 08AR, a lemma

Tag 08AR in the Stacks Project.

AlgebraicGeometry.Space.isCoherent_rightDerived_modulePushforward_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperHigherDirectImageCoherence.lean, line 305. The attribute's comment: “conditional on three cited results carried as explicit hypotheses: Stacks 0720 as h0720 (quasi-coherence of the higher direct images), Stacks 08AN as h08AN (the devissage of coherent modules, with its Noetherian hypothesis on X relaxed to the local Noetherianity that properness supplies) and the third condition of the source's devissage as hwitness (a coherent module with full support on each reduced closed subspace with irreducible point set, whose direct image has coherent higher direct images -- the source gets it from Stacks 089J, 08AQ and 02O4, and Stacks 09YC serves as well). The other two conditions of Stacks 08AN are PROVED here for this property, and so is the local Noetherianity of X”.

Stacks 08AR, with the three cited inputs of the source's proof carried as hypotheses. Let f : X ⟶ Y be a proper morphism of algebraic spaces over S with Y locally Noetherian and let 𝓕 be a coherent 𝒪_X-module. Then R^i f_*𝓕 is a coherent 𝒪_Y-module for every i.

The dévissage h08AN of Stacks 08AN is applied to the property that all higher direct images are coherent. Its local Noetherianity premise is discharged from properness by Stacks 04ZK; its two-out-of-three and finite-sum conditions are AlgebraicGeometry.Space.hasCoherentHigherDirectImages_twoOutOfThree and AlgebraicGeometry.Space.hasCoherentHigherDirectImages_finiteSum, proved above from the long exact sequence of the higher direct images together with Stacks 07UC and Stacks 07UD and consuming the quasi-coherence hypothesis h0720 of Stacks 0720; its integral-subspace condition is hwitness and is not proved.

theorem isCoherent_rightDerived_modulePushforward_of_isProper (f : X ⟶ Y)
    (hf : IsProper B S hS f.hom)
    (hY : HasEtaleLocalProperty B S hS Y.1 (fun V : Scheme.{u} ↦ IsLocallyNoetherian V))
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : IsCoherent B S hS X.1 X.2 F)
    (h0720 : QuasicoherentHigherDirectImages B S hS f)
    (h08AN : CoherentDevissage B S hS X (HasCoherentHigherDirectImages B S hS f))
    (hwitness :
      CoherentDevissageIntegralWitness B S hS X (HasCoherentHigherDirectImages B S hS f))
    (i : ℕ) :
    have := hasInjectiveResolutions_modules B S hS X.1 X.2
    IsCoherent B S hS Y.1 Y.2 (((modulePushforward B S hS f).rightDerived i).obj F)

AlgebraicGeometry.Space.isCoherent_rightDerived_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperHigherDirectImageCoherenceWitness.lean, line 110.

Stacks 08AR. Let f : X ⟶ Y be a proper morphism of algebraic spaces over S with Y locally Noetherian, and let 𝓕 be a coherent 𝒪_X-module. Then R^i f_* 𝓕 is a coherent 𝒪_Y-module for every i ≥ 0.

This is AlgebraicGeometry.Space.isCoherent_rightDerived_of_isProper_of_witness (the reduction to a Noetherian affine base and the dévissage of Stacks 08AN on the source), with the integral witness supplied by AlgebraicGeometry.Space.hasCoherentWitnessOnIntegralSubspaces_of_isProper_of_isAffine.

theorem isCoherent_rightDerived_of_isProper {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y)
    (hf : IsProper B S hS f.hom)
    (hY : HasEtaleLocalProperty B S hS Y.1 (fun V : Scheme.{u} ↦ IsLocallyNoetherian V))
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : IsCoherent B S hS X.1 X.2 F) (n : ℕ) :
    have := hasInjectiveResolutions_modules B S hS X.1 X.2
    IsCoherent B S hS Y.1 Y.2 (((modulePushforward B S hS f).rightDerived n).obj F)

AlgebraicGeometry.Space.isCoherent_higherDirectImage_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperHigherDirectImageCoherent.lean, line 86. References: EGA III (3.2.1), “more general”.

Stacks 08AR. Let f : X ⟶ Y be a proper morphism of algebraic spaces over S with Y locally Noetherian, and let 𝓕 be a coherent 𝒪_X-module. Then R^i f_*𝓕 is a coherent 𝒪_Y-module for every i.

R^i f_*𝓕 is quasi-coherent by Stacks 0720, so by Stacks 07UB it suffices that its sections over every affine étale chart V of Y are finite over 𝒪_Y(V). Those sections are the sections over the identity chart of the restriction of R^i f_*𝓕 to V, which is R^i f'_*(𝓕|_U) for the base change f' : U = V ×_Y X ⟶ V by Stacks 03LX; over the affine scheme V this is R^i Γ(V, f'_* −)(𝓕|_U), the higher direct images of f' being quasi-coherent and hence acyclic over the affine V (Stacks 0720 and 03DW, degenerating the Leray spectral sequence). The base change f' is proper (Stacks 0EPD) and 𝓕|_U is coherent, so AlgebraicGeometry.Space.hasFiniteCohomologyOver_of_isProper applies.

theorem isCoherent_higherDirectImage_of_isProper {X Y : AlgebraicSpaces B S hS}
    (f : X ⟶ Y) (hf : IsProper B S hS f.hom)
    (hY : HasEtaleLocalProperty B S hS Y.1 (fun V : Scheme.{u} ↦ IsLocallyNoetherian V))
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : IsCoherent B S hS X.1 X.2 F) (i : ℕ) :
    have := hasInjectiveResolutions_modules B S hS X.1 X.2
    IsCoherent B S hS Y.1 Y.2 (((modulePushforward B S hS f).rightDerived i).obj F)

Tag 08AS, a lemma

Tag 08AS in the Stacks Project.

AlgebraicGeometry.Space.moduleFinite_cohomologyOverBase_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperCohomologyFinite.lean, line 141. The attribute's comment: “with the finiteness in the degrees below the vanishing bound carried as the hypothesis hlt, that being the one step needing Stacks 08AR, whose higher direct images cannot be written at the module universe of cohomologyOverBase”.

Stacks 08AS. For a Noetherian ring A, a proper algebraic space X over Spec A and a coherent 𝒪_X-module F, every cohomology module Hⁱ(X, F) is a finite A-module: above the vanishing bound N the module is zero, hence finite, and below it finiteness is assumed. Properness and coherence are the hypotheses under which the bound and that finiteness hold and are used nowhere in the proof.

theorem moduleFinite_cohomologyOverBase_of_isProper [IsNoetherianRing A]
    (f : X ⟶ CategoryTheory.yoneda.obj (baseObject A B hA))
    (_hf : IsProper B (Spec (.of A)) hA f)
    (F : Modules.{u, max (u + 1) w} B (Spec (.of A)) hA X hX)
    [IsCoherent B (Spec (.of A)) hA X hX F] (N : ℕ)
    (hvan : ∀ i, N ≤ i → Limits.IsZero (cohomologyOverBase.{u, w} A B hA X hX F i))
    (hlt : ∀ i < N, Module.Finite A (cohomologyOverBase.{u, w} A B hA X hX F i)) (i : ℕ) :
    Module.Finite A (cohomologyOverBase.{u, w} A B hA X hX F i)

AlgebraicGeometry.Space.moduleFinite_cohomologyOverBase_of_isProper_of_isCoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperCohomologyOverBaseFinite.lean, line 68.

Stacks 08AS. Let A be a Noetherian ring, f : X ⟶ Spec A a proper morphism of algebraic spaces and F a coherent 𝒪_X-module. Then Hⁱ(X, F) is a finite A-module for every i ≥ 0.

Here Hⁱ(X, F) is AlgebraicGeometry.Space.cohomologyOverBase, at any module universe max (u + 1) w. F is the universe lift of a coherent module at the universe u of the structure rings, where the finiteness is AlgebraicGeometry.Space.moduleFinite_cohomology_of_isProper (the affine case of Stacks 08AR), and the cohomology over the base of a lift is the lift of the cohomology.

theorem moduleFinite_cohomologyOverBase_of_isProper_of_isCoherent
    (A : Type u) [CommRing A] (B : BigFppfSite.{u}) (hA : B.Contains (Spec (.of A)))
    [IsNoetherianRing A]
    (X : (BigFppfOver B (Spec (.of A)) hA)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B (Spec (.of A)) hA X)
    (f : X ⟶ yoneda.obj (baseObject A B hA)) (hf : IsProper B (Spec (.of A)) hA f)
    (F : Modules.{u, max (u + 1) w} B (Spec (.of A)) hA X hX)
    [IsCoherent B (Spec (.of A)) hA X hX F] (i : ℕ) :
    Module.Finite A (cohomologyOverBase.{u, w} A B hA X hX F i)

AlgebraicGeometry.Space.moduleFinite_cohomology_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperModuleCohomologyFinite.lean, line 297.

Stacks 08AS. Let A be a Noetherian ring, f : X ⟶ Spec A a proper morphism of algebraic spaces and F a coherent 𝒪_X-module. Then Hⁱ(X, F) is a finite A-module for every i ≥ 0.

The right derived functors of Γ(Spec A, f_* −) are finite over the functions on Spec A at a coherent module (AlgebraicGeometry.Space.hasFiniteCohomologyOver_of_isProper, the core of Stacks 08AR), and Γ(Spec A, f_* −) is Γ(X, −) as a functor to A-modules (AlgebraicGeometry.Space.globalSectionsOverBaseIso); restriction of scalars and the universe lift are exact, so they pass through the right derived functors.

theorem moduleFinite_cohomology_of_isProper [IsNoetherianRing A]
    (X : (BigFppfOver B (Spec (.of A)) hA)ᵒᵖ ⥤ Type u)
    (hX : IsAlgebraicSpace B (Spec (.of A)) hA X)
    (f : X ⟶ yoneda.obj (baseObject A B hA)) (hf : IsProper B (Spec (.of A)) hA f)
    (F : Modules.{u, u} B (Spec (.of A)) hA X hX) [IsCoherent B (Spec (.of A)) hA X hX F]
    (i : ℕ) :
    Module.Finite A ((ModuleCat.restrictScalars (baseRingHom A B hA X hX)).obj
      (((globalSectionsFunctor.{u + 1, u, u, u}
        (Stacks.SheafOfModules.Tensor.ringSheaf
          (smallEtaleRingedSite B (Spec (.of A)) hA X hX).O)).rightDerived
          i).obj F))

Tag 08AT, a lemma

Tag 08AT in the Stacks Project.

AlgebraicGeometry.Space.moduleFinite_cohomology_of_isProper_of_algebra, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ProperCohomologyFiniteAlgebra.lean, line 373. The attribute's comment: “ungraded, which is more general: the grading is never used by the proof”.

Stacks 08AT. Let A be a Noetherian ring, R a finitely generated A-algebra and f : X ⟶ Spec A a proper morphism of algebraic spaces. Let F be a quasi-coherent 𝒪_X-module which is a module over f^* R̃ of finite type: an action ρ : R →+* End F restricting on A to multiplication by the scalars, such that over every affine étale chart U of X the sections F(U) are generated over 𝒪(U) by the ρ(R)-translates of finitely many sections. Then Hⁱ(X, F) is a finite R-module for every i.

The source states this for a graded R and a graded module; the grading is not used, and the graded module Hⁱ(X, F) of the source is the cohomology of the total module F here.

theorem moduleFinite_cohomology_of_isProper_of_algebra [IsNoetherianRing A]
    {X : AlgebraicSpaces B (Spec (.of A)) hA} (f : X ⟶ schemeSpace (baseObject A B hA))
    (hf : IsProper B (Spec (.of A)) hA f.hom) (F : Modules.{u, u} B (Spec (.of A)) hA X.1 X.2)
    (hF : F.IsQuasicoherentOnSite) (ρ : R →+* End F)
    (hρ : ∀ a, (ρ (algebraMap A R a)).asHom = globalSmul _ (baseRingHom A B hA X.1 X.2 a) F)
    (hfin : ∀ U : SmallEtale B (Spec (.of A)) hA X.1,
      IsAffine ((SmallEtale.toOver B (Spec (.of A)) hA X.1 ⋙
        BigFppfOver.toScheme B (Spec (.of A)) hA).obj U) →
      ∃ g : Finset (F.val.obj (op U)), Submodule.span (chartRing B (Spec (.of A)) hA X.1 X.2 U)
        {x | ∃ r, ∃ y ∈ g, x = (ρ r).asHom.val.app (op U) y} = ⊤)
    (i : ℕ) :
    letI := (spaceCohomology B (Spec (.of A)) hA X i).endActionModule ρ
    Module.Finite R ((spaceCohomology B (Spec (.of A)) hA X i).obj F)

Sources

Section69.21 Ample invertible sheaves and cohomology #

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

Tag 0GFA, a lemma

Tag 0GFA in the Stacks Project.

AlgebraicGeometry.Space.tfae_isAmple_of_isProper_toAffine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AmpleTwistVanishing.lean, line 302.

Stacks 0GFA. Let X be an algebraic space proper over a Noetherian ring R — here an affine object V of the site with Γ(V, 𝒪_V) = R Noetherian and a proper f : X ⟶ h_V — and let 𝓛 be an invertible 𝒪_X-module. The following are equivalent:

X is a scheme and 𝓛 is ample on it: there are an object U of the site and an isomorphism e : h_U ≅ X for which the restriction of 𝓛 to U is an invertible and ample module;

for every coherent 𝒪_X-module 𝓕 there is an n₀ ≥ 0 with H ᵖ(X, 𝓕 ⊗ 𝓛^{⊗ n}) = 0 for all n ≥ n₀ and p > 0;

for every coherent 𝒪_X-module 𝓕 there is an n ≥ 1 with H¹(X, 𝓕 ⊗ 𝓛^{⊗ n}) = 0.

(1) ⟹ (2) is AlgebraicGeometry.Space.exists_isZero_rightDerived_twistStep_of_isAmple (Serre's vanishing theorem on the scheme, Stacks 0B5T), (2) ⟹ (3) is immediate, and (3) ⟹ (1) is Stacks 0D2W (exists_isAmple_of_forall_isCoherent_isZero_rightDerived_one_twistStep), X being Noetherian as it is proper over a Noetherian affine scheme.

theorem tfae_isAmple_of_isProper_toAffine
    (V : BigFppfOver B S hS) [IsAffine ((BigFppfOver.toScheme B S hS).obj V)]
    [IsNoetherianRing Γ((BigFppfOver.toScheme B S hS).obj V, ⊤)]
    {X : AlgebraicSpaces B S hS} (f : X ⟶ schemeSpace V) (hf : IsProper B S hS f.hom)
    (L : Modules.{u, u} B S hS X.1 X.2)
    [hL : Stacks.SheafOfModules.IsInvertible (structurePresheaf B S hS X.1)
      (Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS X.1 X.2).O).property L] :
    have := enoughInjectives_modules B S hS X.1 X.2
    List.TFAE [
      ∃ (U : BigFppfOver B S hS) (eX : yoneda.obj U ≅ X.1)
        (_ : Stacks.Ample.IsInvertibleModule ((BigFppfOver.toScheme B S hS).obj U)
          (baseChangeModule B S hS L U eX.hom)),
        Stacks.Ample.IsAmple ((BigFppfOver.toScheme B S hS).obj U)
          (baseChangeModule B S hS L U eX.hom),
      ∀ F : Modules.{u, u} B S hS X.1 X.2, IsCoherent B S hS X.1 X.2 F →
        ∃ n₀ : ℕ, ∀ n : ℕ, n₀ ≤ n → ∀ p : ℕ, 0 < p →
          IsZero (((globalSectionsFunctor.{u + 1, u, u, u} (Stacks.SheafOfModules.Tensor.ringSheaf
              (smallEtaleRingedSite B S hS X.1 X.2).O)).rightDerived p).obj
              (twistStep B S hS X.1 X.2 L n F)),
      ∀ F : Modules.{u, u} B S hS X.1 X.2, IsCoherent B S hS X.1 X.2 F →
        ∃ n : ℕ, 1 ≤ n ∧ IsZero (((globalSectionsFunctor.{u + 1, u, u, u}
            (Stacks.SheafOfModules.Tensor.ringSheaf
              (smallEtaleRingedSite B S hS X.1 X.2).O)).rightDerived 1).obj
            (twistStep B S hS X.1 X.2 L n F))]

Tag 0GFB, a lemma

Tag 0GFB in the Stacks Project.

AlgebraicGeometry.Space.exists_isAmple_iff_exists_isAmple_modulePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/AmpleFiniteSurjective.lean, line 241.

Stacks 0GFB. Let R be a Noetherian ring, X an algebraic space proper over R — a proper pX : X ⟶ h_V with V affine and Γ(V, 𝒪_V) = R — and f : Y ⟶ X a finite surjective morphism of algebraic spaces. Let 𝓛 be an invertible 𝒪_X-module. Then X is a scheme and 𝓛 is ample on it if and only if Y is a scheme and f^*𝓛 is ample on it.

A scheme is an object U of the site with an isomorphism h_U ≅ X, and 𝓛 is ample on it when its restriction to U (AlgebraicGeometry.Space.baseChangeModule) is invertible and ample. The source also assumes Y proper over R; that follows, a finite morphism being proper.

theorem exists_isAmple_iff_exists_isAmple_modulePullback
    (V : BigFppfOver B S hS) [IsAffine ((BigFppfOver.toScheme B S hS).obj V)]
    [IsNoetherianRing Γ((BigFppfOver.toScheme B S hS).obj V, ⊤)]
    {X Y : AlgebraicSpaces B S hS} (pX : X ⟶ schemeSpace V) (hpX : IsProper B S hS pX.hom)
    (f : Y ⟶ X) (hf : IsFinite B S hS f.hom) (hfs : IsSurjective B S hS f.hom)
    (L : Modules.{u, u} B S hS X.1 X.2)
    [hL : Stacks.SheafOfModules.IsInvertible (structurePresheaf B S hS X.1)
      (Stacks.SheafOfModules.Tensor.ringSheaf (smallEtaleRingedSite B S hS X.1 X.2).O).property L] :
    (∃ (U : BigFppfOver B S hS) (eX : yoneda.obj U ≅ X.1)
      (_ : Stacks.Ample.IsInvertibleModule ((BigFppfOver.toScheme B S hS).obj U)
        (baseChangeModule B S hS L U eX.hom)),
      Stacks.Ample.IsAmple ((BigFppfOver.toScheme B S hS).obj U)
        (baseChangeModule B S hS L U eX.hom)) ↔
    ∃ (U' : BigFppfOver B S hS) (eY : yoneda.obj U' ≅ Y.1)
      (_ : Stacks.Ample.IsInvertibleModule ((BigFppfOver.toScheme B S hS).obj U')
        (baseChangeModule B S hS ((modulePullback B S hS f).obj L) U' eY.hom)),
      Stacks.Ample.IsAmple ((BigFppfOver.toScheme B S hS).obj U')
        (baseChangeModule B S hS ((modulePullback B S hS f).obj L) U' eY.hom)

Sources

LeanAlgebraicGeometry.Space.tfae_isAmple_of_isProper_toAffine · AlgebraicGeometry.Space.exists_isAmple_iff_exists_isAmple_modulePullback

Section69.22 The theorem on formal functions #

Section 69.22 of the Stacks Project, Tag 08AU. 10 tags here are carried by 28 declarations of the repository (all in StacksFrontier) and 7 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 08AU, the section

Tag 08AU in the Stacks Project.

AlgebraicGeometry.Space.FormalFunctionsSituation.idealPowerMultiple, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormalFunctionsIdealPower.lean, line 82. The attribute's comment: “the submodule Iⁿℱ of ℱ generated as an 𝒪_X-module by products of local sections of ℱ and elements of Iⁿ, in Situation 08AV”.

The submodule Iⁿℱ of Situation 08AV (Section 08AU): the submodule of ℱ generated by the products of local sections of ℱ and elements of Iⁿ, the image of multiplication by the global functions coming from Iⁿ.

abbrev idealPowerMultiple (n : ℕ) :
    Modules.{u, max (u + 1) w} S.site (Spec (.of S.ring)) S.containsBase S.space.1 S.space.2

AlgebraicGeometry.Space.FormalFunctionsSituation.isQuasicoherentOnSite_idealPowerSubmodule, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormalFunctionsIdealPower.lean, line 140. The attribute's comment: “Iⁿℱ is a quasi-coherent submodule of ℱ, in Situation 08AV”.

Iⁿℱ is quasi-coherent (Section 08AU): it is the image of a morphism from a direct sum of copies of the coherent, hence quasi-coherent, module ℱ to ℱ; a direct sum of quasi-coherent modules is quasi-coherent (Stacks 03M1 (1)) and so is the image of a morphism of quasi-coherent modules (Stacks 03M1 (3)).

theorem isQuasicoherentOnSite_idealPowerSubmodule (n : ℕ) :
    (idealPowerSubmodule S n).IsQuasicoherentOnSite

AlgebraicGeometry.Space.FormalFunctionsSituation.imageSubobject_idealPowerTensorMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormalFunctionsIdealPowerImage.lean, line 518. The attribute's comment: “Iⁿℱ is the image of f^Ĩⁿ ⊗ ℱ → ℱ, in Situation 08AV; the source writes f^Ĩ for the ideal Iⁿ of the submodule Iⁿℱ”.

Iⁿℱ is the image of f^*Ĩⁿ ⊗_{𝒪_X} ℱ ⟶ ℱ (Section 08AU), in Situation 08AV: as subobjects of ℱ, the image of the map f^*Ĩⁿ ⊗ ℱ ⟶ 𝒪_X ⊗ ℱ ≅ ℱ is the submodule Iⁿℱ generated by the products of local sections of ℱ and elements of Iⁿ.

theorem imageSubobject_idealPowerTensorMap (n : ℕ) :
    imageSubobject (idealPowerTensorMap S n) = Subobject.mk (idealPowerSubmoduleι S n)

AlgebraicGeometry.Space.FormalFunctionsSituation.idealPowerSubmodule_spec, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormalFunctionsIdealPowerImage.lean, line 540. The attribute's comment: “Iⁿℱ is a quasi-coherent submodule of ℱ and is the image of f^*Ĩⁿ ⊗ ℱ → ℱ, in Situation 08AV”.

Section 08AU, in Situation 08AV: the submodule Iⁿℱ of ℱ generated by the products of local sections of ℱ and elements of Iⁿ is quasi-coherent, and it is the image of the map f^*Ĩⁿ ⊗_{𝒪_X} ℱ ⟶ ℱ.

theorem idealPowerSubmodule_spec (n : ℕ) :
    (idealPowerSubmodule S n).IsQuasicoherentOnSite ∧
      imageSubobject (idealPowerTensorMap S n) = Subobject.mk (idealPowerSubmoduleι S n)

Tag 08AV, a situation

Tag 08AV in the Stacks Project.

AlgebraicGeometry.Space.FormalFunctionsSituation, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormalFunctions.lean, line 57.

Stacks 08AV. A Noetherian ring A with an ideal I, a proper algebraic space over Spec A, and a coherent module on that space.

structure FormalFunctionsSituation

Tag 08AW, a lemma

Tag 08AW in the Stacks Project.

AlgebraicGeometry.Space.isReesFinite_cohomologyIdealPowerSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IdealPowerCohomologyReesFinite.lean, line 821. References: SGA 2 XII (5.8), “(ii), special case”.

Stacks 08AW. In Situation 08AV — A Noetherian, I ⊆ A an ideal, f : X ⟶ Spec A proper and F a coherent 𝒪_X-module — for every p the graded module ⨁ₙ Hᵖ(X, Iⁿ F) is a finite module over the Rees algebra B = ⨁ₙ Iⁿ.

The graded module structure is that of the Rees system cohomologyIdealPowerSystem: an element a ∈ Iᵏ acts as the cohomology of multiplication by a, from Iⁿ F to Iᵏ⁺ⁿ F.

theorem isReesFinite_cohomologyIdealPowerSystem [IsNoetherianRing A]
    (f : X ⟶ schemeSpace (baseObject A B hA)) (hf : IsProper B (Spec (.of A)) hA f.hom)
    (F : Modules.{u, u} B (Spec (.of A)) hA X.1 X.2) [hF : IsCoherent B (Spec (.of A)) hA X.1 X.2 F]
    (I : Ideal A) (p : ℕ) :
    (cohomologyIdealPowerSystem (baseRingHom A B hA X.1 X.2) F I p).IsReesFinite

Tag 08AX, a lemma

Tag 08AX in the Stacks Project.

AlgebraicGeometry.Space.exists_surjective_cohomologyIdealPowerMul_and_range_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/IdealPowerCohomologyReesFinite.lean, line 840.

Stacks 08AX. In Situation 08AV — A Noetherian, I ⊆ A an ideal, f : X ⟶ Spec A proper and F a coherent 𝒪_X-module — for every p there is an integer c ≥ 0 such that

the multiplication map Iⁿ⁻ᶜ ⊗ Hᵖ(X, Iᶜ F) ⟶ Hᵖ(X, Iⁿ F) is surjective for all n ≥ c, here written for n = m + c;

the image of Hᵖ(X, Iⁿ⁺ᵐ F) ⟶ Hᵖ(X, Iⁿ F) is contained in Iᵐ⁻ᶜ Hᵖ(X, Iⁿ F) for all n ≥ 0 and m ≥ c.

theorem exists_surjective_cohomologyIdealPowerMul_and_range_le [IsNoetherianRing A]
    (f : X ⟶ schemeSpace (baseObject A B hA)) (hf : IsProper B (Spec (.of A)) hA f.hom)
    (F : Modules.{u, u} B (Spec (.of A)) hA X.1 X.2) [IsCoherent B (Spec (.of A)) hA X.1 X.2 F]
    (I : Ideal A) (p : ℕ) :
    ∃ c : ℕ, (∀ m : ℕ, Function.Surjective (TensorProduct.lift
        (cohomologyIdealPowerMul (baseRingHom A B hA X.1 X.2) F I p m c le_rfl))) ∧
      ∀ n m : ℕ, c ≤ m →
        LinearMap.range (cohomologyIdealPowerTr (baseRingHom A B hA X.1 X.2) F I p
          (Nat.le_add_right n m)) ≤
          I ^ (m - c) • (⊤ : Submodule A
            (cohomologyIdealPower (baseRingHom A B hA X.1 X.2) F I p n))

Tag 08AY, a lemma

Tag 08AY in the Stacks Project.

Stacks.AdicCohomologyBound.ker_le_pow_smul_top, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohomologyAdicUniformBounds.lean, line 140. The attribute's comment: “clause (1): ker(H^p(X,F) -> H^p(X,F/I^n F)) is contained in I^(n-c) H^p(X,F) for n >= c. The two inputs of the source's two-step proof are hypotheses, neither being available in this repository: hexactM is exactness of the long exact sequence of 0 -> I^n F -> F -> F/I^n F -> 0 at H^p(X,F), and h08AX is clause (2) of Tag 08AX at n = 0. The cohomology modules are arbitrary A-modules for the same reason”.

Clause (1) of [Stacks, Tag 08AY].

In Situation 08AV, for a fixed p there is a c with ker (H ᵖ (X, ℱ) ⟶ H ᵖ (X, ℱ / I ⁿ ℱ)) ⊆ I ^ (n - c) H ᵖ (X, ℱ) for all n ≥ c.

The source's proof is two steps. The long exact sequence of 0 ⟶ I ⁿ ℱ ⟶ ℱ ⟶ ℱ / I ⁿ ℱ ⟶ 0 identifies that kernel with the image of H ᵖ (X, I ⁿ ℱ) ⟶ H ᵖ (X, ℱ), which is the hypothesis hexactM here; and clause (2) of [Stacks, Tag 08AX], taken at n = 0, bounds that image by I ^ (n - c) H ᵖ (X, ℱ), which is the hypothesis h08AX. Only the containment ker (π n) ⊆ im (ι n) is needed, not the equality the source writes.

theorem ker_le_pow_smul_top {Λ : ℕ → Type*} [∀ n, AddCommGroup (Λ n)] [∀ n, Module A (Λ n)]
    {Q : ℕ → Type*} [∀ n, AddCommGroup (Q n)] [∀ n, Module A (Q n)]
    (ι : ∀ n, Λ n →ₗ[A] M) (π : ∀ n, M →ₗ[A] Q n) (c : ℕ)
    (hexactM : ∀ n, LinearMap.ker (π n) ≤ LinearMap.range (ι n))
    (h08AX : ∀ n, c ≤ n → LinearMap.range (ι n) ≤ I ^ (n - c) • (⊤ : Submodule A M)) :
    ∀ n, c ≤ n → LinearMap.ker (π n) ≤ I ^ (n - c) • (⊤ : Submodule A M)

Stacks.AdicCohomologyBound.exists_range_transition_eq_range_proj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohomologyAdicUniformBounds.lean, line 170. The attribute's comment: “clause (3): for each n there is c2 >= n with im(H^p(X,F/I^k F) -> H^p(X,F/I^n F)) = im(H^p(X,F) -> H^p(X,F/I^n F)) for k >= c2. The source's Artin-Rees argument, proved in full; its four inputs are hypotheses, none available here: the ladder of long exact sequences, Tag 08AX clause (2) for H^(p+1), finiteness from Tag 08AR, and the annihilation of H^p(X,F/I^n F) by I^n. As in the source c2 grows with n: NOT of form n + c”.

Clause (3) of [Stacks, Tag 08AY].

In Situation 08AV, for a fixed p and a fixed n there is a c₂ ≥ n with im (H ᵖ (X, ℱ / I ᵏ ℱ) ⟶ H ᵖ (X, ℱ / I ⁿ ℱ)) = im (H ᵖ (X, ℱ) ⟶ H ᵖ (X, ℱ / I ⁿ ℱ)) for all k ≥ c₂.

The containment of the image of π n in the image of T n k is the compatibility hπ of the restriction maps with the transitions. For the other containment, the source's argument runs as follows. Let x = T n k y. The ladder of long exact sequences gives δ n x = U n k (δ k y), so δ n x lies in the image of U n k, which clause (2) of [Stacks, Tag 08AX] for H ᵖ⁺¹ bounds by I ^ N L n with N = k - n - c. Artin–Rees for the submodule im (δ n) ⊆ L n produces a constant c₃ with im (δ n) ⊓ I ^ N L n ⊆ δ n (I ^ (N - c₃) Q n) for N ≥ c₃; and I ⁿ annihilates Q n, so once N - c₃ ≥ n that target submodule is zero. Hence δ n x = 0, and exactness at H ᵖ (X, ℱ / I ⁿ ℱ) puts x in the image of π n. The threshold produced is c₂ = 2 * n + c + c₃; see this file's implementation notes for why it cannot be brought down to n + c for a single c.

theorem exists_range_transition_eq_range_proj [IsNoetherianRing A]
    {Q : ℕ → Type*} [∀ n, AddCommGroup (Q n)] [∀ n, Module A (Q n)]
    {L : ℕ → Type*} [∀ n, AddCommGroup (L n)] [∀ n, Module A (L n)]
    (π : ∀ n, M →ₗ[A] Q n) (T : ∀ m n : ℕ, m ≤ n → Q n →ₗ[A] Q m)
    (δ : ∀ n, Q n →ₗ[A] L n) (U : ∀ m n : ℕ, m ≤ n → L n →ₗ[A] L m) (c : ℕ)
    (hfin : ∀ n, Module.Finite A (L n))
    (hπ : ∀ (m n : ℕ) (h : m ≤ n), (T m n h).comp (π n) = π m)
    (hladder : ∀ (m n : ℕ) (h : m ≤ n), (δ m).comp (T m n h) = (U m n h).comp (δ n))
    (hexact : ∀ n, LinearMap.ker (δ n) ≤ LinearMap.range (π n))
    (hann : ∀ n, I ^ n • (⊤ : Submodule A (Q n)) = ⊥)
    (h08AXconnecting : ∀ (n k : ℕ) (h : n ≤ k), n + c ≤ k →
      LinearMap.range (U n k h) ≤ I ^ (k - n - c) • (⊤ : Submodule A (L n)))
    (n : ℕ) :
    ∃ c₂ : ℕ, n ≤ c₂ ∧ ∀ (k : ℕ) (h : n ≤ k), c₂ ≤ k →
      LinearMap.range (T n k h) = LinearMap.range (π n)

Stacks.AdicCohomologyBound.exists_range_transition_stable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohomologyAdicUniformBounds.lean, line 216. The attribute's comment: “clause (2) in elementary form -- the images of the transition maps of the tower H^p(X,F/I^n F) stabilize -- deduced from clause (3) exactly as the source does, the hypothesis being the conclusion of exists_range_transition_eq_range_proj above”.

Clause (2) of [Stacks, Tag 08AY], in elementary form.

"Part (3) implies part (2) by definition of the Mittag-Leffler condition": once the image of T n k equals the image of π n for all k ≥ c₂, those images are in particular all equal to one another, which is the stabilization asserted by [Stacks, Tag 02N0]. The hypothesis here is precisely the conclusion of exists_range_transition_eq_range_proj.

theorem exists_range_transition_stable {Q : ℕ → Type*} [∀ n, AddCommGroup (Q n)]
    [∀ n, Module A (Q n)] (π : ∀ n, M →ₗ[A] Q n) (T : ∀ m n : ℕ, m ≤ n → Q n →ₗ[A] Q m)
    (h : ∀ n : ℕ, ∃ c₂ : ℕ, n ≤ c₂ ∧ ∀ (k : ℕ) (hnk : n ≤ k), c₂ ≤ k →
      LinearMap.range (T n k hnk) = LinearMap.range (π n))
    (n : ℕ) :
    ∃ c₂ : ℕ, ∃ hnc₂ : n ≤ c₂, ∀ (k : ℕ) (hnk : n ≤ k), c₂ ≤ k →
      LinearMap.range (T n k hnk) = LinearMap.range (T n c₂ hnc₂)

Stacks.AdicCohomologyBound.isMittagLefflerCategorical_of_exists_range_eq_range_proj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohomologyAdicUniformBounds.lean, line 242. The attribute's comment: “clause (2) in the vocabulary of Tag 02N0: the tower H^p(X,F/I^n F), presented as a functor into ModuleCat, satisfies IsMittagLefflerCategorical. Deduced from clause (3), whose conclusion is the hypothesis h; the stabilized value is the image of the restriction map from H^p(X,F)”.

Clause (2) of [Stacks, Tag 08AY], in the vocabulary of [Stacks, Tag 02N0].

For the tower n ↦ H ᵖ (X, ℱ / I ⁿ ℱ) presented as an inverse system of A-modules, that is a functor F : ℕᵒᵖ ⥤ ModuleCat A, clause (3) of [Stacks, Tag 08AY] says that the images of the transition maps into F.obj (op n) are eventually the image of π n; so they stabilize, which is the Mittag-Leffler condition IsMittagLefflerCategorical of [Stacks, Tag 02N0]. The passage from ranges of linear maps to the transition subobjects that the definition speaks of is the dictionary isMittagLefflerCategorical_of_range_eq_submodule.

theorem isMittagLefflerCategorical_of_exists_range_eq_range_proj {A : Type u} [Ring A]
    {M : Type w} [AddCommGroup M] [Module A M] (F : ℕᵒᵖ ⥤ ModuleCat.{v} A)
    (π : ∀ n : ℕ, M →ₗ[A] F.obj (op n))
    (h : ∀ n : ℕ, ∃ c₂ : ℕ, n ≤ c₂ ∧ ∀ (k : ℕ) (hnk : n ≤ k), c₂ ≤ k →
      LinearMap.range (F.map (homOfLE hnk).op).hom = LinearMap.range (π n)) :
    IsMittagLefflerCategorical F

AlgebraicGeometry.Space.exists_ker_cohomologyIdealQuotientProj_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohomologyAdicUniformBoundsSpace.lean, line 101. The attribute's comment: “clause (1)”.

Stacks 08AY, clause (1). In Situation 08AV, for every p there is a c₁ ≥ 0 such that ker (Hᵖ(X, F) ⟶ Hᵖ(X, F / Iⁿ F)) ⊆ Iⁿ⁻ᶜ¹ Hᵖ(X, F) for all n ≥ c₁.

theorem exists_ker_cohomologyIdealQuotientProj_le [IsNoetherianRing A]
    (f : X ⟶ schemeSpace (baseObject A B hA)) (hf : IsProper B (Spec (.of A)) hA f.hom)
    (F : Modules.{u, u} B (Spec (.of A)) hA X.1 X.2) [IsCoherent B (Spec (.of A)) hA X.1 X.2 F]
    (I : Ideal A) (p : ℕ) :
    ∃ c₁ : ℕ, ∀ n : ℕ, c₁ ≤ n →
      LinearMap.ker (C1573.cohomologyIdealQuotientProj (baseRingHom A B hA X.1 X.2) F I p n) ≤
        I ^ (n - c₁) • (⊤ : Submodule A (cohomologyRes (baseRingHom A B hA X.1 X.2) p F))

AlgebraicGeometry.Space.exists_range_cohomologyIdealQuotientTr_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohomologyAdicUniformBoundsSpace.lean, line 114. The attribute's comment: “clause (3)”.

Stacks 08AY, clause (3). In Situation 08AV, for every p and every n there is a c₂(n) ≥ n such that im (Hᵖ(X, F / Iᵏ F) ⟶ Hᵖ(X, F / Iⁿ F)) = im (Hᵖ(X, F) ⟶ Hᵖ(X, F / Iⁿ F)) for all k ≥ c₂(n).

theorem exists_range_cohomologyIdealQuotientTr_eq [IsNoetherianRing A]
    (f : X ⟶ schemeSpace (baseObject A B hA)) (hf : IsProper B (Spec (.of A)) hA f.hom)
    (F : Modules.{u, u} B (Spec (.of A)) hA X.1 X.2) [hF : IsCoherent B (Spec (.of A)) hA X.1 X.2 F]
    (I : Ideal A) (p n : ℕ) :
    ∃ c₂ : ℕ, n ≤ c₂ ∧ ∀ (k : ℕ) (h : n ≤ k), c₂ ≤ k →
      LinearMap.range (C1573.cohomologyIdealQuotientTr (baseRingHom A B hA X.1 X.2) F I p h) =
        LinearMap.range (C1573.cohomologyIdealQuotientProj (baseRingHom A B hA X.1 X.2) F I p n)

AlgebraicGeometry.Space.isMittagLefflerCategorical_cohomologyIdealQuotientTower, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/CohomologyAdicUniformBoundsSpace.lean, line 126. The attribute's comment: “clause (2)”.

Stacks 08AY, clause (2). In Situation 08AV, for every p the inverse system (Hᵖ(X, F / Iⁿ F))ₙ satisfies the Mittag-Leffler condition.

theorem isMittagLefflerCategorical_cohomologyIdealQuotientTower [IsNoetherianRing A]
    (f : X ⟶ schemeSpace (baseObject A B hA)) (hf : IsProper B (Spec (.of A)) hA f.hom)
    (F : Modules.{u, u} B (Spec (.of A)) hA X.1 X.2) [IsCoherent B (Spec (.of A)) hA X.1 X.2 F]
    (I : Ideal A) (p : ℕ) :
    IsMittagLefflerCategorical
      (C1573.cohomologyIdealQuotientTower (baseRingHom A B hA X.1 X.2) F I p)

Declarations registered for the tag:

AlgebraicGeometry.Space.C1573.exists_ker_cohomologyIdealQuotientProj_le, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/FormalFunctionsGeometricStalkLimit.lean, line 521 (StacksFrontier): “clause (1)”.
AlgebraicGeometry.Space.C1573.exists_range_cohomologyIdealQuotientTr_eq, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/FormalFunctionsGeometricStalkLimit.lean, line 523 (StacksFrontier): “clause (3)”.
AlgebraicGeometry.Space.C1573.isMittagLefflerCategorical_cohomologyIdealQuotientTower, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/FormalFunctionsGeometricStalkLimit.lean, line 525 (StacksFrontier): “clause (2)”.

Tag 08AZ, a theorem

Tag 08AZ in the Stacks Project.

AlgebraicGeometry.Space.SiteAdicCohomology.adicCompletionEquivCohomologyTower, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormalFunctionsAdicLimit.lean, line 392. The attribute's comment: “the isomorphism of A-modules only, NOT the homeomorphism for the limit topologies, which is not proved anywhere in this file; for an arbitrary site, generalizing Situation 08AV; granted the bundled hb : IsAdicCohomologyBound, whose two fields ker_le and range_eq are exactly Tag 08AY clauses (1) and (3), the latter with its per-n level”.

Stacks Project, Tag 08AZ, the isomorphism clause, for an arbitrary site and granted [Stacks, Tag 08AY].

With 𝒪 a sheaf of commutative rings on a site C, I an ideal of a ring A mapping to the global functions by φ and ℱ an 𝒪-module, the I-adic completion of H ^ p (C, ℱ) is the limit of the tower n ↦ H ^ p (C, ℱ / I ^ n ℱ). That the isomorphism is the one defined by the system of maps H ^ p (C, ℱ) / I ^ n H ^ p (C, ℱ) ⟶ H ^ p (C, ℱ / I ^ n ℱ) of the source's statement is adicCompletionEquivCohomologyTower_proj_of.

This is more general than Situation 08AV, which is the case of the small étale ringed site of a proper algebraic space over Spec A with a coherent module on it; that case is AlgebraicGeometry.Space.FormalFunctionsSituation.formalFunctionsEquiv. The properness, coherence and Noetherian hypotheses of Situation 08AV enter the source's proof only through [Stacks, Tag 08AY], which is carried here as the hypothesis hb, so they are not needed separately and the statement generalizes.

[Stacks, Tag 08AZ] further asserts that the comparison is a homeomorphism for the limit topologies. That clause is not proved and is not claimed by any declaration in this file.

The containment I ^ n H ^ p (C, ℱ) ⊆ ker (H ^ p (C, ℱ) ⟶ H ^ p (C, ℱ / I ^ n ℱ)) is reproved in place rather than taken from pow_smul_top_le_ker_cohomologyAdicProj: passing that lemma in makes the elaborator compare its statement with the one the tower comparison asks for through the ModuleCat coercions of the cohomology modules, which does not terminate.

def adicCompletionEquivCohomologyTower : CohomologyAdicComparison O φ I F p

AlgebraicGeometry.Space.SiteAdicCohomology.adicCompletionEquivCohomologyTower_proj_of, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormalFunctionsAdicLimit.lean, line 444. The attribute's comment: “the identification of the isomorphism as the one DEFINED BY the system of maps H^p(X, F)/I^n H^p(X, F) -> H^p(X, F/I^n F) of the statement, rather than merely an abstract isomorphism of the two limits; same carried hypothesis hb : IsAdicCohomologyBound (Tag 08AY clauses (1) and (3)); again nothing about the limit topologies”.

The comparison isomorphism is the canonical one: its n-th component carries the image in H ^ p (C, ℱ)^∧_I of a class x to the image of x in H ^ p (C, ℱ / I ^ n ℱ). Together with adicCompletionEquivCohomologyTower this says that the system of maps H ^ p (C, ℱ) / I ^ n H ^ p (C, ℱ) ⟶ H ^ p (C, ℱ / I ^ n ℱ) is what defines the isomorphism of limits, rather than merely that the two modules are isomorphic.

This is the second assertion of the isomorphism clause of [Stacks, Tag 08AZ], for an arbitrary site; Situation 08AV is the case of the small étale ringed site of a proper algebraic space over Spec A with a coherent module on it, and nothing here asserts the homeomorphism of limit topologies.

lemma adicCompletionEquivCohomologyTower_proj_of (n : ℕ) :
    IsDefinedByProjections O φ I F p c hb n

AlgebraicGeometry.Space.FormalFunctionsSituation.formalFunctionsEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormalFunctionsAdicLimit.lean, line 604. The attribute's comment: “IN SITUATION 08AV: the isomorphism of A-modules only, NOT the homeomorphism for the limit topologies, which is nowhere claimed here; granted the one bundled hypothesis h08AY : Is08AYBound S p c, whose two fields ker_le and range_eq are exactly Tag 08AY clauses (1) and (3), the latter with its per-n level; Situation 08AV's hypotheses are fields of S”.

Stacks Project, Tag 08AZ in Situation 08AV, the isomorphism clause, granted [Stacks, Tag 08AY].

In Situation 08AV — A Noetherian, I ⊆ A an ideal, f : X ⟶ Spec A a proper morphism of algebraic spaces and ℱ a coherent 𝒪_X-module, all of them fields of S — the I-adic completion of H ^ p (X, ℱ) is the limit of the tower n ↦ H ^ p (X, ℱ / I ^ n ℱ). The cohomology is AlgebraicGeometry.Space.cohomologyOverBase (cohomology_eq, cohomologyTower_eq) and the thickenings are the quotients of ℱ by the subsheaf generated by the I ^ n-multiples of its sections (adicThickening).

What is carried. The hypothesis h08AY is the conjunction of clauses (1) and (3) of [Stacks, Tag 08AY]; see Is08AYBound. [Stacks, Tag 08AY] is not proved in this file. Clause (2) of that lemma, the Mittag-Leffler condition, is not needed: in this formulation clause (3) subsumes it. The standing hypotheses of Situation 08AV are what make [Stacks, Tag 08AY] true and are used nowhere else in the argument, which is why h08AY is the only hypothesis beyond the situation itself.

What is not proved. [Stacks, Tag 08AZ] further asserts that the comparison is a homeomorphism for the limit topologies. That clause is not proved, and no declaration in this file claims it; neither side is given a topology here.

Everything else is proved: the thickenings and their transition maps are constructed, I ^ n is shown to annihilate H ^ p (X, ℱ / I ^ n ℱ), and the passage from those facts to the comparison is AlgebraicGeometry.Space.SiteAdicCohomology.adicCompletionEquivCohomologyTower, which runs the source's own argument through Stacks.IntertwinedFiltration.adicCompletionEquivTowerLimitOfEventualRange.

The body is written with have and exact rather than as a direct term: elaborating the specialization against the expected type makes the elaborator reduce the module structures of the cohomology groups at the small étale ringed site, which does not terminate, whereas elaborating it first and matching the two syntactically equal types afterwards is immediate.

def formalFunctionsEquiv : Comparison S p

AlgebraicGeometry.Space.FormalFunctionsSituation.formalFunctionsEquiv_proj_of, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormalFunctionsAdicLimit.lean, line 633. The attribute's comment: “IN SITUATION 08AV: the identification of the isomorphism of formalFunctionsEquiv as the one DEFINED BY the system of maps H^p(X, F)/I^n H^p(X, F) -> H^p(X, F/I^n F) of the statement; same carried hypothesis h08AY : Is08AYBound S p c (Tag 08AY clauses (1) and (3)); again nothing about the limit topologies”.

The comparison isomorphism of [Stacks, Tag 08AZ] in Situation 08AV 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, ℱ / I ^ n ℱ).

Together with formalFunctionsEquiv this is the assertion of [Stacks, Tag 08AZ] that the system of maps H ^ p (X, ℱ) / I ^ n H ^ p (X, ℱ) ⟶ H ^ p (X, ℱ / I ^ n ℱ) is what defines the isomorphism of limits, rather than merely that the two modules are isomorphic.

Carried: the same single hypothesis h08AY, clauses (1) and (3) of [Stacks, Tag 08AY]. Not claimed: the homeomorphism for the limit topologies.

lemma formalFunctionsEquiv_proj_of (n : ℕ) : IsDefinedBy08AZProjections S p c h08AY n

AlgebraicGeometry.Space.formalFunctionsEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormalFunctionsAdicLimitUnconditional.lean, line 115. The attribute's comment: “the isomorphism of limits”.

Stacks 08AZ, the isomorphism. In Situation 08AV, for every p the maps Hᵖ(X, F) / Iⁿ Hᵖ(X, F) ⟶ Hᵖ(X, F / Iⁿ F) define an isomorphism Hᵖ(X, F)^∧ ⟶ lim_n Hᵖ(X, F / Iⁿ F) from the I-adic completion; that it is defined by those maps is formalFunctionsEquiv_apply.

def formalFunctionsEquiv :
    AdicCompletion I (cohomologyRes (baseRingHom A B hA X.1 X.2) p F) ≃ₗ[A]
      C1573.cohomologyIdealQuotientLimit (baseRingHom A B hA X.1 X.2) F I p

AlgebraicGeometry.Space.formalFunctionsEquiv_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormalFunctionsAdicLimitUnconditional.lean, line 124. The attribute's comment: “the isomorphism is the one defined by the system of maps”.

Stacks 08AZ, the isomorphism is the one defined by the system of maps: the n-th component of the image of w ∈ Hᵖ(X, F)^∧ is the image of the n-th component of w under Hᵖ(X, F) / Iⁿ Hᵖ(X, F) ⟶ Hᵖ(X, F / Iⁿ F).

theorem formalFunctionsEquiv_apply
    (w : AdicCompletion I (cohomologyRes (baseRingHom A B hA X.1 X.2) p F)) (n : ℕ) :
    ((formalFunctionsEquiv f hf F I p w : C1573.cohomologyIdealQuotientLimit _ F I p) :
      ∀ k, C1573.cohomologyIdealQuotient (baseRingHom A B hA X.1 X.2) F I p k) n =
      C1573.adicQuotientMap _
        (C1573.cohomologyIdealQuotientProj (baseRingHom A B hA X.1 X.2) F I p) I
        (C1573.pow_smul_top_le_ker_cohomologyIdealQuotientProj _ F I p) n (w.val n)

AlgebraicGeometry.Space.isHomeomorph_formalFunctionsEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormalFunctionsAdicLimitUnconditional.lean, line 136. The attribute's comment: “the isomorphism is a homeomorphism for the limit topologies”.

Stacks 08AZ, the homeomorphism: the comparison is a homeomorphism for the limit topologies.

theorem isHomeomorph_formalFunctionsEquiv :
    @IsHomeomorph _ _
      (C1573.adicCompletionLimitTopology I (cohomologyRes (baseRingHom A B hA X.1 X.2) p F))
      (C1573.towerLimitTopology _ _) (formalFunctionsEquiv f hf F I p)

Declarations registered for the tag:

AlgebraicGeometry.Space.C1573.formalFunctionsEquiv, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/FormalFunctionsGeometricStalkLimit.lean, line 527 (StacksFrontier): “the isomorphism of limits”.
AlgebraicGeometry.Space.C1573.formalFunctionsEquiv_apply, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/FormalFunctionsGeometricStalkLimit.lean, line 528 (StacksFrontier): “the isomorphism is the one defined by the system of maps”.
AlgebraicGeometry.Space.C1573.isHomeomorph_formalFunctionsEquiv, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/FormalFunctionsGeometricStalkLimit.lean, line 530 (StacksFrontier): “the isomorphism is a homeomorphism for the limit topologies”.

Tag 08B0, a lemma

Tag 08B0 in the Stacks Project.

AlgebraicGeometry.Space.bijective_cohomologyToIdealQuotientLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormalFunctionsAdicLimitUnconditional.lean, line 147.

Stacks 08B0. Let A be a Noetherian ring complete with respect to an ideal I, f : X ⟶ Spec A a proper morphism of algebraic spaces and F a coherent 𝒪_X-module. Then Hᵖ(X, F) ⟶ lim_n Hᵖ(X, F / Iⁿ F) is an isomorphism for every p.

theorem bijective_cohomologyToIdealQuotientLimit [IsAdicComplete I A] :
    Function.Bijective
      (C1573.cohomologyToIdealQuotientLimit (baseRingHom A B hA X.1 X.2) F I p)

AlgebraicGeometry.Space.cohomologyToIdealQuotientLimit_bijective_of_isAdicComplete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormalFunctionsIdealQuotientLimit.lean, line 82. References: EGA III (4.1.5), “partial”; EGA III (4.1.7), “special case”; SGA 2 XII (5.8), “partial”.

Stacks 08B0. Let A be a Noetherian ring ([IsNoetherianRing A]), I ⊆ A an ideal such that A is I-adically complete ([IsAdicComplete I A]), f : X ⟶ Spec A a proper morphism of algebraic spaces and F a coherent 𝒪_X-module. Then for every p ≥ 0 the canonical map Hᵖ(X, F) ⟶ lim_n Hᵖ(X, F / Iⁿ F) is bijective, i.e. Hᵖ(X, F) = lim_n Hᵖ(X, F / Iⁿ F).

The objects in the statement, with the files that define them: * B : BigFppfSite is a big fppf site and hA : B.Contains (Spec A) says that Spec A is one of its schemes; AlgebraicSpaces B (Spec A) hA (StacksFrontier/AlgebraicGeometry/Spaces/Category.lean) is the category of algebraic spaces over Spec A. * AlgebraicGeometry.Space.baseObject A B hA (StacksFrontier/AlgebraicGeometry/Spaces/FormalAlgebraization.lean) is Spec A itself as an object of the big fppf site over Spec A (the identity of Spec A), and AlgebraicGeometry.schemeSpace (StacksFrontier/AlgebraicGeometry/Spaces/SchemeAsSpace.lean) regards it as an algebraic space, so f : X ⟶ schemeSpace (baseObject A B hA) is a morphism X ⟶ Spec A of algebraic spaces over Spec A. * AlgebraicGeometry.Space.IsProper (StacksFrontier/AlgebraicGeometry/Spaces/UniversallyClosed.lean, Stacks 03ZM) is properness of a morphism of algebraic spaces: separated, of finite type and universally closed. * AlgebraicGeometry.Space.Modules (StacksFrontier/AlgebraicGeometry/Spaces/RingedSite.lean) is the category of 𝒪_X-modules on the small étale site of X, and AlgebraicGeometry.Space.IsCoherent (StacksFrontier/AlgebraicGeometry/Spaces/CoherentModules.lean, Stacks 07UA) says that such a module is coherent. * AlgebraicGeometry.Space.baseRingHom A B hA X.1 X.2 (StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleCohomology.lean) is the canonical ring map from A to the global functions of X, through which A acts on cohomology. * AlgebraicGeometry.Space.C1573.cohomologyToIdealQuotientLimit φ F I p (the imported module) is the A-linear map Hᵖ(X, F) ⟶ lim_n Hᵖ(X, F / Iⁿ F) whose n-th component is the map on Hᵖ induced by the projection F ⟶ F / Iⁿ F. Here Hᵖ(X, -) is the p-th right derived functor of global sections on 𝒪_X-modules, as an A-module along φ (AlgebraicGeometry.Space.cohomologyRes, StacksFrontier/AlgebraicGeometry/Spaces/IdealPowerCohomologyReesFinite.lean); F / Iⁿ F is the cokernel of the inclusion of the submodule Iⁿ F ⊆ F, the image of multiplication by the elements of Iⁿ (AlgebraicGeometry.Space.idealQuotient, StacksFrontier/AlgebraicGeometry/Spaces/IdealMultipleModule.lean); and the limit is AlgebraicGeometry.Space.C1573.cohomologyIdealQuotientLimit (same file as the map), the A-module of compatible families of the tower n ↦ Hᵖ(X, F / Iⁿ F) under the maps induced by F / Iⁿ F ⟶ F / Iᵐ F, m ≤ n (Stacks.IntertwinedFiltration.towerLimit, StacksFrontier/RingTheory/AdicCompletion/IntertwinedFiltration.lean).

The proof is AlgebraicGeometry.Space.C1573.bijective_cohomologyToIdealQuotientLimit: Hᵖ(X, F) is a finite A-module (Stacks 08AS), hence I-adically complete, and the theorem on formal functions (Stacks 08AZ) identifies its completion with the limit.

theorem cohomologyToIdealQuotientLimit_bijective_of_isAdicComplete {B : BigFppfSite.{u}}
    {A : Type u} [CommRing A] [IsNoetherianRing A] {hA : B.Contains (Spec (.of A))}
    {X : AlgebraicSpaces B (Spec (.of A)) hA} (f : X ⟶ schemeSpace (baseObject A B hA))
    (hf : IsProper B (Spec (.of A)) hA f.hom) (F : Modules.{u, u} B (Spec (.of A)) hA X.1 X.2)
    [IsCoherent B (Spec (.of A)) hA X.1 X.2 F] (I : Ideal A) [IsAdicComplete I A] (p : ℕ) :
    Function.Bijective
      (C1573.cohomologyToIdealQuotientLimit (baseRingHom A B hA X.1 X.2) F I p)

Declarations registered for the tag:

AlgebraicGeometry.Space.C1573.bijective_cohomologyToIdealQuotientLimit, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/FormalFunctionsGeometricStalkLimit.lean, line 532 (StacksFrontier).

Tag 08B1, a lemma

Tag 08B1 in the Stacks Project.

AlgebraicGeometry.Space.completionIsoLimitOfQuotients_geometricStalk_of_towerIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormalFunctionsGeometricStalk.lean, line 351. The attribute's comment: “the restriction maps assemble into an isomorphism (R^p f_* ℱ)_ȳ^∧ ≅ lim_n H^p(X_n, ℱ_n) of 𝒪_{Y,ȳ}-modules, granted Tag 08AZ, which is absent from this repository: 08AZ's own conclusion for the tower H^p(X', ℱ'/𝔪^n ℱ') is the hypothesis h08AZ, and its identification with the tower H^p(X_n, ℱ_n) -- Tag 073K clause (1) plus Tag 07UH and Leray, none of them proved here -- is the hypothesis e. The tower is data because the X_n need Tag 04KF to be formed at the universe of the site. Neither the homeomorphism of limit topologies nor 𝒪_{Y,ȳ}^∧-linearity is asserted”.

[Stacks, Tag 08B1], granted [Stacks, Tag 08AZ], and for the 𝒪_{Y, ȳ}-module isomorphism only.

Let f : X ⟶ Y be a proper morphism of algebraic spaces over a scheme S with Y locally Noetherian, let ℱ be a coherent 𝒪_X-module and let ȳ be a geometric point of Y. Write 𝔪 for the maximal ideal of 𝒪_{Y, ȳ} and M = (R ᵖ f_* ℱ)_ȳ. Let P be the tower n ↦ H ᵖ (X_n, ℱ_n) of the source, with transition maps T and restriction maps π. Then the π n assemble into an isomorphism M ^∧_𝔪 ≅ lim_n H ᵖ (X_n, ℱ_n).

Carried: the tower Q of [Stacks, Tag 08AZ] — the cohomology H ᵖ (X', ℱ'/𝔪 ⁿ ℱ') on the base change X' = Spec 𝒪_{Y, ȳ} ×_Y X — with its projections ρ out of M, the conclusion of [Stacks, Tag 08AZ] for it as the single hypothesis h08AZ, and the identification e of Q with P, which is the combination of [Stacks, Tag 073K] and [Stacks, Tag 07UH] that the source's last two sentences perform. Proved: that these give the statement. See the implementation notes of this file for why each of the three is unavailable here, and for the two refinements of the source's conclusion — the homeomorphism of limit topologies and 𝒪_{Y, ȳ} ^∧-linearity — that are not claimed.

theorem completionIsoLimitOfQuotients_geometricStalk_of_towerIso
    {X : AlgebraicSpaces B S hS} (f : X ⟶ Y) (_hf : IsProper B S hS f.hom)
    (F : Modules.{u, u} B S hS X.obj X.property)
    (_hF : IsCoherent B S hS X.obj X.property F) (p : ℕ)
    (Q : ℕ → Type*) [∀ n, AddCommGroup (Q n)]
    [∀ n, Module (etaleLocalRing B S hS Y.obj y) (Q n)]
    (U : ∀ m n : ℕ, m ≤ n → Q n →ₗ[etaleLocalRing B S hS Y.obj y] Q m)
    (ρ : ∀ n, moduleHigherPushforwardGeometricStalk B S hS f F p y
      →ₗ[etaleLocalRing B S hS Y.obj y] Q n)
    (P : ℕ → Type*) [∀ n, AddCommGroup (P n)]
    [∀ n, Module (etaleLocalRing B S hS Y.obj y) (P n)]
    (T : ∀ m n : ℕ, m ≤ n → P n →ₗ[etaleLocalRing B S hS Y.obj y] P m)
    (π : ∀ n, moduleHigherPushforwardGeometricStalk B S hS f F p y
      →ₗ[etaleLocalRing B S hS Y.obj y] P n)
    (h08AZ : CompletionIsoLimitOfQuotients (geometricMaximalIdeal B S hS Y y)
      (moduleHigherPushforwardGeometricStalk B S hS f F p y) Q U ρ)
    (e : ∀ n, Q n ≃ₗ[etaleLocalRing B S hS Y.obj y] P n)
    (he : ∀ (m n : ℕ) (h : m ≤ n) (x : Q n), T m n h (e n x) = e m (U m n h x))
    (hπ : ∀ (n : ℕ) (x : moduleHigherPushforwardGeometricStalk B S hS f F p y),
      π n x = e n (ρ n x)) :
    CompletionIsoLimitOfQuotients (geometricMaximalIdeal B S hS Y y)
      (moduleHigherPushforwardGeometricStalk B S hS f F p y) P T π

AlgebraicGeometry.Space.completionIsoLimitOfQuotients_geometricStalk_of_bounds, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormalFunctionsGeometricStalk.lean, line 395. The attribute's comment: “the same conclusion by the second route: the bounds Tag 08AY supplies for the tower H^p(X_n, ℱ_n) are carried as h08AY_ker and h08AY_range, which are now exactly 08AY clauses (1) and (3) -- clause (3) with the per-n level the source states, not a uniform shift -- and the comparison is DERIVED from them; the annihilation hypothesis hann discharges the third input of the limit argument. Same two refinements not asserted as in the first route”.

[Stacks, Tag 08B1], granted the bounds of [Stacks, Tag 08AY] for the tower of the source, and for the 𝒪_{Y, ȳ}-module isomorphism only.

The second route of this file: rather than carrying the conclusion of [Stacks, Tag 08AZ] and transporting it, carry for the tower P = H ᵖ (X_n, ℱ_n) itself the two bounds that [Stacks, Tag 08AY] provides — clause (1), a bound ker (π n) ⊆ 𝔪 ^ (n - c) M for n ≥ c, and clause (3), that for each n the images of the transition maps into P n are the image of π n from some level c₂ ≥ n on — and derive the comparison from the commutative-algebra core Stacks.IntertwinedFiltration.adicCompletionEquivTowerLimitOfEventualRange. The two carried hypotheses are exactly those two clauses, in the shape Stacks.AdicCohomologyBound.ker_le_pow_smul_top and Stacks.AdicCohomologyBound.exists_range_transition_eq_range_proj state them; in particular the level in clause (3) depends on n and is not tied to c. The remaining hypothesis of the core, 𝔪 ⁿ M ⊆ ker (π n), is deduced here from the annihilation hann of H ᵖ (X_n, ℱ_n) by 𝔪 ⁿ, which holds because X_n lives over Spec (𝒪_{Y, ȳ}/𝔪 ⁿ).

theorem completionIsoLimitOfQuotients_geometricStalk_of_bounds
    {X : AlgebraicSpaces B S hS} (f : X ⟶ Y) (_hf : IsProper B S hS f.hom)
    (F : Modules.{u, u} B S hS X.obj X.property)
    (_hF : IsCoherent B S hS X.obj X.property F) (p : ℕ) (c : ℕ)
    (P : ℕ → Type*) [∀ n, AddCommGroup (P n)]
    [∀ n, Module (etaleLocalRing B S hS Y.obj y) (P n)]
    (T : ∀ m n : ℕ, m ≤ n → P n →ₗ[etaleLocalRing B S hS Y.obj y] P m)
    (π : ∀ n, moduleHigherPushforwardGeometricStalk B S hS f F p y
      →ₗ[etaleLocalRing B S hS Y.obj y] P n)
    (hπ : ∀ (m n : ℕ) (h : m ≤ n), (T m n h).comp (π n) = π m)
    (hann : ∀ n, geometricMaximalIdeal B S hS Y y ^ n •
      (⊤ : Submodule (etaleLocalRing B S hS Y.obj y) (P n)) = ⊥)
    (h08AY_ker : ∀ n : ℕ, c ≤ n → LinearMap.ker (π n) ≤
      geometricMaximalIdeal B S hS Y y ^ (n - c) •
        (⊤ : Submodule (etaleLocalRing B S hS Y.obj y)
          (moduleHigherPushforwardGeometricStalk B S hS f F p y)))
    (h08AY_range : ∀ n : ℕ, ∃ c₂ : ℕ, n ≤ c₂ ∧ ∀ (k : ℕ) (h : n ≤ k), c₂ ≤ k →
      LinearMap.range (T n k h) = LinearMap.range (π n)) :
    CompletionIsoLimitOfQuotients (geometricMaximalIdeal B S hS Y y)
      (moduleHigherPushforwardGeometricStalk B S hS f F p y) P T π

AlgebraicGeometry.Space.completionIsoLimitOfQuotientsOverCompletion_geometricStalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FormalFunctionsGeometricStalkLimit.lean, line 489.

The theorem on formal functions at a geometric point, [Stacks, Tag 08B1].

Let f : X ⟶ Y be a proper morphism of algebraic spaces over S with Y locally Noetherian, let F be a coherent 𝒪_X-module, ȳ a geometric point of Y, and let X_n = Spec (𝒪_{Y, ȳ} / 𝔪 ⁿ) ×_Y X be the infinitesimal neighbourhoods of the geometric fibre (AlgebraicGeometry.Space.isPullback_geometricInfinitesimalNeighbourhood), with F_n the pullback of F. Then

(R ᵖ f_* F)_ȳ ^∧ ≅ lim_n H ᵖ (X_n, F_n)

as modules over 𝒪_{Y, ȳ} ^∧: there is an isomorphism of modules over R = Γ(Spec 𝒪_{Y, ȳ}, 𝒪) ≅ 𝒪_{Y, ȳ} from the 𝔪-adic completion of the stalk to the limit, whose n-th component on the image of the stalk is the map (R ᵖ f_* F)_ȳ ⟶ H ᵖ (X_n, F_n), and which is linear over the completion R ^∧, acting on lim_n H ᵖ (X_n, F_n) through R ^∧ ⟶ R / 𝔪 ⁿ.

theorem completionIsoLimitOfQuotientsOverCompletion_geometricStalk (hf : IsProper B S hS f.hom)
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : IsCoherent B S hS X.1 X.2 F) (p : ℕ) :
    CompletionIsoLimitOfQuotientsOverCompletion (maximalIdeal Γ((BigFppfOver.toScheme B S hS).obj
        (etaleLocalRingSpecObject (y := y) hY), ⊤))
      ((ModuleCat.restrictScalars (etaleLocalRingSpecFunctionsEquiv y hY).toRingHom).obj
        (geometricModuleStalk B S hS Y y (moduleHigherPushforward B S hS f F p)))
      (fun n => geometricInfinitesimalNeighbourhoodCohomology f y hY F p n)
      (geometricInfinitesimalNeighbourhoodTransition f y hY F hF.toIsQuasicoherentOnSite p)
      (geometricInfinitesimalNeighbourhoodProj f y hY hf F hF.toIsQuasicoherentOnSite p)
      (geometricInfinitesimalNeighbourhoodCohomology_smul_eq_zero f y hY F
        hF.toIsQuasicoherentOnSite p)

Tag 0A4S, a lemma

Tag 0A4S in the Stacks Project.

AlgebraicGeometry.Space.subsingleton_moduleHigherPushforwardGeometricStalk_of_discreteTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/HigherDirectImageStalkVanishing.lean, line 408.

Stacks 0A4S: stalks of higher direct images vanish when the fibre is discrete. Let f : X ⟶ Y be a proper morphism of algebraic spaces over S with Y locally Noetherian, let ȳ be a geometric point of Y such that the geometric fibre X_ȳ = Spec κ(ȳ) ×_Y X has discrete underlying topological space, and let ℱ be a coherent 𝒪_X-module. Then (Rᵖ f_* ℱ)_ȳ = 0 for every p > 0: the fibre, locally of finite type over a field with discrete underlying space, has dimension at most 0, and Stacks 0A4T applies.

theorem subsingleton_moduleHigherPushforwardGeometricStalk_of_discreteTopology
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (hf : IsProper B S hS f.hom)
    (hY : HasEtaleLocalProperty B S hS Y.1 (fun V : Scheme.{u} ↦ IsLocallyNoetherian V))
    (y : GeometricPoint B S hS Y.1)
    (hdisc : DiscreteTopology (points B S hS (pullback (yonedaEquiv.symm y.val.value) f.hom)))
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : IsCoherent B S hS X.1 X.2 F) (p : ℕ) (hp : 0 < p) :
    Subsingleton (moduleHigherPushforwardGeometricStalk B S hS f F p y)

Tag 0A4T, a lemma

Tag 0A4T in the Stacks Project.

AlgebraicGeometry.Space.subsingleton_moduleHigherPushforwardGeometricStalk_of_dimension_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/HigherDirectImageStalkVanishing.lean, line 375.

Stacks 0A4T: stalks of higher direct images vanish above the dimension of the fibre. Let f : X ⟶ Y be a proper morphism of algebraic spaces over S with Y locally Noetherian, let ȳ be a geometric point of Y such that the geometric fibre X_ȳ = Spec κ(ȳ) ×_Y X has dimension at most d, and let ℱ be a coherent 𝒪_X-module. Then (Rᵖ f_* ℱ)_ȳ = 0 for every p > d.

By the theorem on formal functions at ȳ (Stacks 08B1) the completion of the finite module (Rᵖ f_* ℱ)_ȳ over the Noetherian local ring 𝒪_{Y, ȳ} is lim_n Hᵖ(X_n, ℱ_n), and each term vanishes by AlgebraicGeometry.Space.subsingleton_geometricInfinitesimalNeighbourhoodCohomology; a finite module over a Noetherian local ring embeds in its completion.

theorem subsingleton_moduleHigherPushforwardGeometricStalk_of_dimension_le
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (hf : IsProper B S hS f.hom)
    (hY : HasEtaleLocalProperty B S hS Y.1 (fun V : Scheme.{u} ↦ IsLocallyNoetherian V))
    (y : GeometricPoint B S hS Y.1) (d : WithBot ℕ∞)
    (hd : dimension B S hS (pullback (yonedaEquiv.symm y.val.value) f.hom)
      (isAlgebraicSpace_pullback B S hS (yonedaEquiv.symm y.val.value) f.hom
        (isAlgebraicSpace_yoneda B S hS (y.val.siteObject B S hS Y.1)) X.2 Y.2) ≤ d)
    (F : Modules.{u, u} B S hS X.1 X.2) (hF : IsCoherent B S hS X.1 X.2 F) (p : ℕ) (hp : d < p) :
    Subsingleton (moduleHigherPushforwardGeometricStalk B S hS f F p y)

Sources

LeanAlgebraicGeometry.Space.FormalFunctionsSituation.idealPowerMultiple · AlgebraicGeometry.Space.FormalFunctionsSituation.isQuasicoherentOnSite_idealPowerSubmodule · AlgebraicGeometry.Space.FormalFunctionsSituation.imageSubobject_idealPowerTensorMap · AlgebraicGeometry.Space.FormalFunctionsSituation.idealPowerSubmodule_spec · AlgebraicGeometry.Space.FormalFunctionsSituation · AlgebraicGeometry.Space.isReesFinite_cohomologyIdealPowerSystem · AlgebraicGeometry.Space.exists_surjective_cohomologyIdealPowerMul_and_range_le · Stacks.AdicCohomologyBound.ker_le_pow_smul_top

Section69.23 Applications of the theorem on formal functions #

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

Tag 0A4V, a lemma

Tag 0A4V in the Stacks Project.

AlgebraicGeometry.Space.isFinite_iff_isProper_and_discreteFibres, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteProperDiscreteFibres.lean, line 64.

Stacks 0A4V. A morphism f : X ⟶ Y of algebraic spaces over S is finite exactly when it is proper and the point space of its fibre over every field-valued point of Y is discrete.

The source assumes Y locally Noetherian; the equivalence holds for every target, as conditions (1) and (3) of Stacks 0A4X.

theorem isFinite_iff_isProper_and_discreteFibres
    (spaceX : IsAlgebraicSpace B S hS X) (spaceY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y) :
    IsFinite B S hS f ↔
      IsProper B S hS f ∧ ∀ p : FieldValuedPoint B S hS Y,
        DiscreteTopology (points B S hS (pullback (yonedaEquiv.symm p.value) f))

Tag 0A4W, a lemma

Tag 0A4W in the Stacks Project.

AlgebraicGeometry.Space.exists_isOpenSubspace_isFinite_pullback_snd_of_finite_geometricFibre, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteNearFiniteGeometricFibre.lean, line 79.

Stacks 0A4W. Let f : X ⟶ Y be a proper morphism of algebraic spaces over S and let ȳ be a geometric point of Y whose geometric fibre X_ȳ has finitely many points. Then ȳ has an open neighbourhood V ⊆ Y over which f becomes finite, in the sense that the base change f^{-1}(V) ⟶ V is finite.

The source assumes Y locally Noetherian; the conclusion holds for every target. A proper morphism is decent, so the finite fibre X_ȳ has discrete point space by Stacks 0ACK, hence f is quasi-finite at every point of |X| over the image of ȳ, and Stacks 0A4Y applies.

theorem exists_isOpenSubspace_isFinite_pullback_snd_of_finite_geometricFibre
    (spaceX : IsAlgebraicSpace B S hS X) (spaceY : IsAlgebraicSpace B S hS Y) (f : X ⟶ Y)
    (proper : IsProper B S hS f) (y : GeometricPoint B S hS Y)
    (finiteFibre : Finite (points B S hS (pullback f (yonedaEquiv.symm y.val.value)))) :
    ∃ V : Subfunctor Y, IsOpenSubspace B S hS V ∧
      y.image ∈ Set.range (pointsMap B S hS V.toFunctor V.ι) ∧
      IsFinite B S hS (pullback.snd f V.ι)

Sources

LeanAlgebraicGeometry.Space.isFinite_iff_isProper_and_discreteFibres · AlgebraicGeometry.Space.exists_isOpenSubspace_isFinite_pullback_snd_of_finite_geometricFibre

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

69.16 Vanishing of cohomology to 69.23 Applications of the…

Section69.16 Vanishing of cohomology#

Tag 07UY, a situation

Tag 07UZ, a lemma

Tag 07V0, a lemma

Tag 07V1, a lemma

Tag 07V4, a lemma

Tag 07V5, a lemma

Tag 07V6, a proposition

Tag 0D2V, a lemma

Tag 0D2W, a lemma

Sources

Section69.17 Finite morphisms and affines#

Tag 0GF7, a lemma

Tag 0GF8, a lemma

Tag 07VP, a lemma

Sources

Section69.18 A weak version of Chow's lemma#

Tag 089J, a lemma

Sources

Section69.19 Noetherian valuative criterion#

Tag 0ARJ, a lemma

Tag 0ARK, a lemma

Tag 0ARL, a remark

Sources

Section69.20 Higher direct images of coherent sheaves#

Tag 08AQ, a lemma

Tag 08AR, a lemma

Tag 08AS, a lemma

Tag 08AT, a lemma

Sources

Section69.21 Ample invertible sheaves and cohomology#

Tag 0GFA, a lemma

Tag 0GFB, a lemma

Sources

Section69.22 The theorem on formal functions#

Tag 08AU, the section

Tag 08AV, a situation

Tag 08AW, a lemma

Tag 08AX, a lemma

Tag 08AY, a lemma

Tag 08AZ, a theorem

Tag 08B0, a lemma

Tag 08B1, a lemma

Tag 0A4S, a lemma

Tag 0A4T, a lemma

Sources

Section69.23 Applications of the theorem on formal functions#

Tag 0A4V, a lemma

Tag 0A4W, a lemma

Sources

Section69.16 Vanishing of cohomology #

Section69.17 Finite morphisms and affines #

Section69.18 A weak version of Chow's lemma #

Section69.19 Noetherian valuative criterion #

Section69.20 Higher direct images of coherent sheaves #

Section69.21 Ample invertible sheaves and cohomology #

Section69.22 The theorem on formal functions #

Section69.23 Applications of the theorem on formal functions #